Verasco, a formally verified C static analyzer

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.

Speaker Details

Jacques-Henri Jourdan is currently a PhD student in computer science at Inria Paris, under the direction of Xavier Leroy. During his PhD, he was one of the main developers of Verasco, a formally proved C static analyzer. He is planning to defend in February or March 2016. Before his PhD, he worked in the RiSE team at MSR Redmond on the CodeContracts static checker for .Net, as part of an internship with Francesco Logozzo. He is also the author of the formally verified C99 Parser of the CompCert compiler.

Date:
Speakers:
Jacques Henri Jourdan
Affiliation:
INRIA Paris

    • Portrait of Jeff Running

      Jeff Running