Verasco is a static analyzer for the CompCert subset of ISO C 1999 that establishes the absence of run-time errors in analyzed programs. The analyzer is based on abstract interpretation and combines several abstract domains, non-relational (integer intervals, floating-point intervals, integer congruences, points-to properties) and relational (integer linear inequalities, symbolic equalities). Verasco enjoys a modular structure roughly inspired by that of Astrée.
The major novelty of Verasco, compared with other static analysis tools, is that it is entirely specified and proved sound using the Coq proof assistant. Verasco's proof guarantees, with mathematical certainty, that programs that analyze without alarms are free of run-time errors.
To compile, you will need:
- Any patch level of the Coq proof assistant version 8.4.
- The OCaml functional language, version 4.00 or later.
- The following OCaml libraries and tools:
- The Menhir parser generator.
- The ZArith library.
- The Ocamlfind tool.
The Verasco analyzer reuses parts of the CompCert verified C compiler and therefore is not free software. This release can be used for evaluation, research and education purposes, but not for commercial purposes. However, the Coq sources specific to the Verasco static analyzer are dual-licensed under the GNU Public Licence (GPL) and can be reused freely in other projects subject to the terms of the GPL. See the License for more information.
The following paper describes the design, architecture, and verification of the Verasco analyzer:
A Formally-Verified C Static Analyzer, by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. In POPL 2015, 42nd ACM symposium on Principles of Programming Languages.
The VPL library that implements Verasco's polyhedral abstract domain is described in the following papers:
Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra, by Alexis Fouilhé, David Monniaux, and Michaël Périn. In 20th Static Analysis Symposium (SAS 2013), LNCS 7935, Springer, 2013.
A certifying frontend for (sub)polyhedral abstract domains, by Alexis Fouilhé and Sylvain Boulmé. In Verified Software: Theories, Tools and Experiments (VSTTE) 2014. LNCS 8471, Springer. 2014.
Other related publications are available on the Verasco project pages.
The Verasco project
The Verasco analyzer is developed as part of ANR project Verasco (ANR-11-INSE-003). This project investigates the formal verification of static analyzers and of compilers, two families of tools that play a crucial role in the development and validation of critical embedded software. The project partners are: Inria Paris-Rocquencourt (coordinator), Airbus, Université Rennes 1, VERIMAG, and Inria Saclay.