The SAMS Verification Environment
The SAMS verification environment is a tool for the functional verification of MISRA-C programs. It was developed on top of the theorem prover Isabelle during the course of the SAMS project. The C source code is annotated, e.g. with function pre- and postconditions, and the correctness is proven interactively.
The verification environment comprises a frontend, which checks conformance to the MISRA guidelines, and translates the C sources to Isabelle, and a semantic backend, with which the annotated specifications can be verified. The following diagram shows the dataflow (generated files are filled in grey):
To learn more about the SAMS verification environment:
- Watch a demonstration video (in German, sorry!) showing verification at work on a simple example, or
- read the paper Certifiable specification and verification of C programs (or visit our talk at FM'09), or
- study the reference manual (again, in German), which explains syntax and semantics of the annotations, and defines the supported C constructs.
Download
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.
