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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00: IIIHILT at Franklin
Chair(s): Peter ChapinVermont Technical College
15:30 - 16:00
Short-paper
HILT
16:00 - 16:30
Short-paper
HILT
P: Dara LyCEA LIST, Nikolai KosmatovCEA List, Frederic LoulergueNorthern Arizona University, Julien SignolesCEA LIST
16:30 - 16:55
Short-paper
HILT
P: Andrew BernsUniversity of Northern Iowa, James CurbowUniversity of Northern Iowa, Joshua HilliardUniversity of Northern Iowa, Sheriff JorkehUniversity of Northern Iowa, Miho SandersUniversity of Northern Iowa
16:55 - 17:00
Social Event
HILT