Die Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Verwaltung des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Mathematik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Universität Bremen


INHALT & PFAD:
Startseite Detail


Verification of Real-World C Programs with VCC



Datum: 28.10.2009

Ort: Cartesium Rotunde


Vortragende(r): Dr. Markus Dahlweid (European Microsoft Innovation Center, Aachen, Germany)





Abstract

VCC is an industrial-strength verification environment for low-level concurrent system code written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove the correctness of these annotations. It includes tools for monitoring proof attempts and constructing partial counterexample executions for failed proofs.
This talk motivates VCC, describes our verification methodology, describes the architecture of VCC, and reports on our experience using VCC to verify the Microsoft Hyper-V hypervisor. VCC has been released as an open source project at http://vcc.codeplex.com.


CV

Markus Dahlweid wrote his PhD thesis “High Level Transition Systems of CSP Specifications” at Bremen University. After completing his studies Markus worked at Verified Systems as software development and testing engineer in the area of safety-critical embedded systems. He currently works a researcher at the European Microsoft Innovation Center (EMIC) in Aachen on verifying the Microsoft Hyper-V Hypervisor kernel as part of the Verisoft XT research project funded by BMBF and developing the verification tools needed to verify C code.








zurück  

Seitenanfang  -  Impressum Zuletzt geändert durch: birgit [b]   20.11.2009 Admin-Login