| Verifying C Compilier |
|
|
|
| VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity. |
| < Prev | Next > |
|---|
Upcoming Public Events:
- Oct 04-08 Linux Device Drivers - in German or English (Munich)
- Oct 20-21 Embedded Live 2010 - English (London)
- Nov 08-13 EGLiSA - in German or English (Munich)
With your technical knowledge you are kind of ambidextrous in your domain
