Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Verasco, a formally verified C static analyzer
Speaker:Jacques-Henri Jourdan
coming from:INRIA
Speakers Bio:
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Expert Audience
Language:English
Date, Time and Location
Date:Wednesday, 6 January 2016
Time:13:00
Duration:60 Minutes
Location:Kaiserslautern
Building:G26
Room:111
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
Name(s):Brigitta Hansen
Phone:0681 93039102
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbr├╝cken
To Building:E1 5To Room:005
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created by:Brigitta Hansen/MPI-SWS, 01/04/2016 03:46 PMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Brigitta Hansen, 01/04/2016 03:49 PM -- Created document.