Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Tue 20 Sep 2016 17:15 - 17:40 at Noh Theater - Session 8 Chair(s): Scott Owens

Abstract interpretation provides advanced techniques to infer numerical invariants on programs. There is an abundant literature about numerical abstract domains that operate on scalar variables. This work deals with lifting these techniques to a realistic C memory model. We present an abstract memory functor that takes as argument any standard numerical abstract domain, and builds a memory abstract domain that finely tracks properties about memory contents, taking into account union types, pointer arithmetic and type casts. This functor is implemented and verified inside the Coq proof assistant with respect to the CompCert compiler memory model. Using the Coq extraction mechanism, it is fully executable and used by the Verasco C static analyzer.

Tue 20 Sep

icfp-2016-papers
16:50 - 17:40: Research Papers - Session 8 at Noh Theater
Chair(s): Scott OwensUniversity of Kent, UK
icfp-2016-papers16:50 - 17:15
Talk
David DaraisUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA
DOI
icfp-2016-papers17:15 - 17:40
Talk
Sandrine BlazyUniversity of Rennes 1, France, Vincent LaporteIMDEA Software Institute, Spain, David PichardieENS Rennes, France
DOI