MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Verasco, a formally verified C static analyzer

Jacques-Henri Jourdan
INRIA
SWS Colloquium
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
Expert Audience
English

Date, Time and Location

Wednesday, 6 January 2016
13:00
60 Minutes
G26
111
Kaiserslautern

Abstract


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.

Contact

Brigitta Hansen
0681 93039102
--email hidden

Video Broadcast

Yes
Saarbrücken
E1 5
005
passcode not visible
logged in users only

Brigitta Hansen, 01/04/2016 15:49 -- Created document.