• Main
• Software
• Berichte
• Verification
• Demonstrator
• Publications
• Contact

Software

Current Releases

• The safety component, packaged up as a library.

The verification environment comprises two components, which can be downloaded here:

• The Isabelle theories, which allow you to do the actual correctness proof, and
• the C frontend, which translates annotated C-Programs into Isabelle theories.

For the Isabelle theories, you need Isabelle 2009, for the C frontend the Haskell-Compiler and Cabal.

Past releases

These are kept for historic and reference purpose, and are not supported anymore.

Version 0.96

This version offers a more concise specification of the calculation of the safety zone.

• The safety component (note this is just the bare source code, for actual use the packaged library above is better suited).
• The proof scripts. To run them, you need the verification environment Isabelle theories and Isabelle 2009.

Version 0.9

This is the version released to TÜV, and which was the basis of the certification. Note most documents are in German.

• The safety component (note this is just the bare source code, for actual use the packaged library above is better suited).
• The proof scripts. To run them, you need the verification environment Isabelle theories and Isabelle 2009.
• The C-Frontend (needs ghc 6.10 and various packages such as HaXml to compile; no Cabal support).