- static analyzer for the CompCert subset of ISO C 1999 that establishes the absence of run-time errors in analyzed programs
- entirely specified and proved sound using the Coq proof assistant
- http://compcert.inria.fr/verasco/
Tags:
tool
native
Last modified 17 February 2026