Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Tue 17 Jan 2017 14:30 - 15:00 at Amphitheater 44 - Abstract Interpretation Chair(s): Roberto Giacobazzi

We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undefined behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design eva, an abstract interpreter for C implemented within the frama framework. We present the domains that are available so far within eva, and show that this communication mechanism is able to handle them seamlessly.

Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30: Abstract InterpretationVMCAI at Amphitheater 44
Chair(s): Roberto GiacobazziUniversity of Verona, Italy
14:00 - 14:30
Complete Abstractions and Subclassical Modal Logics
Vijay D'SilvaGoogle, Marcelo SousaUniversity of Oxford
14:30 - 15:00
Structuring Abstract Interpreters through State and Value Abstractions
David BühlerCEA LIST, Boris YakobowskiCEA - LIST, Sandrine BlazyUniversity of Rennes 1, France
Media Attached
15:00 - 15:30
Conjunctive Abstract Interpretation using Paramodulation
Mooly SagivTel Aviv University, A: Or OzeriTel Aviv university, Oded PadonTel Aviv University, Noam RinetzkyTel Aviv University
Media Attached