BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verasco\, a formally verified C static analyzer  - Jacques Henri J
 ourdan\, INRIA Paris
DTSTART:20160111T093000Z
DTEND:20160111T103000Z
UID:TALK63441@talks.cam.ac.uk
CONTACT:44515
DESCRIPTION:This talk will present the design and soundness proof of Veras
 co\, a formally verified static analyzer for most of the ISO C99 language 
 (excluding recursion and dynamic allocation)\, developed using the Coq pro
 of assistant. Verasco aims at establishing the absence of run-time errors 
 in the analyzed programs. It enjoys a modular architecture that supports t
 he extensible combination of multiple abstract domains\, both relational a
 nd non-relational. It include a memory abstract domain\, an abstract domai
 n of arithmetical symbolic equalities\, an abstract domain of intervals\, 
 an abstract domain of arithmetical congruences and an octagonal abstract d
 omain. \nVerasco 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 ov
 er to the compiled code. \n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR