This talk will present the design and soundness proof of Verasco, a
formally verified static analyzer for most of the ISO C99 language
(excluding recursion and dynamic allocation), developed using the Coq
proof assistant. Verasco aims at establishing the absence of run-time
errors in the analyzed programs. It enjoys a modular architecture that
supports the extensible combination of multiple abstract domains, both
relational and non-relational. It include a memory abstract domain, an
abstract domain of arithmetical symbolic equalities, an abstract domain
of intervals, an abstract domain of arithmetical congruences and an
octagonal abstract domain.
Verasco integrates with the CompCert formally-verified C compiler so
that not only the soundness of the analysis results is guaranteed with
mathematical certitude, but also the fact that these guarantees carry
over to the compiled code.