C-to-Isabelle parser: You are downloading a tool and set of theories for Isabelle/HOL. This tool translates a large subset of C99 code into the imperative language Simpl embedded in the theorem prover Isabelle/HOL. This language provides a verified verification condition generator and further tools for software verification. This tool is used to verify the functional correctness of the seL4 microkernel and some other programs, as part of the L4.verified project.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Dodds, Josiah; Appel, Andrew W.: Mostly sound type system improves a foundational program verifier (2013)