Mon 5 Nov 2018 16:00 - 16:30 at Franklin - III Chair(s): Peter Chapin

An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g. their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.

Mon 5 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00
IIIHILT at Franklin
Chair(s): Peter Chapin Vermont Technical College
15:30
30m
Short-paper
SPARK by Example: an introduction to formal verification through the standard C++ library
HILT
Léo Creuse ISAE, Joffrey Huguet ISAE, P: Christophe Garion ISAE-SUPAERO, Jerome Hugues ISAE
16:00
30m
Short-paper
Soundness of a Dataflow Analysis for Memory Monitoring
HILT
P: Dara Ly CEA LIST, Nikolai Kosmatov CEA List, Frederic Loulergue Northern Arizona University, Julien Signoles CEA LIST
16:30
25m
Short-paper
Minimal Specifications for Detecting Security Vulnerabilities
HILT
P: Andrew Berns University of Northern Iowa, James Curbow University of Northern Iowa, Joshua Hilliard University of Northern Iowa, Sheriff Jorkeh University of Northern Iowa, Miho Sanders University of Northern Iowa
16:55
5m
Social Event
6:30PM HILT Banquet at Legal Seafoods, Park Plaza, preceded by SIGAda EC meeting from 5:15 to 6:15PM
HILT