Structuring Abstract Interpreters through State and Value Abstractions
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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | Abstract InterpretationVMCAI at Amphitheater 44 Chair(s): Roberto Giacobazzi University of Verona, Italy | ||
14:00 30mTalk | Complete Abstractions and Subclassical Modal Logics VMCAI | ||
14:30 30mTalk | Structuring Abstract Interpreters through State and Value Abstractions VMCAI Media Attached | ||
15:00 30mTalk | Conjunctive Abstract Interpretation using Paramodulation VMCAI Mooly Sagiv Tel Aviv University, A: Or Ozeri Tel Aviv university, Oded Padon Tel Aviv University, Noam Rinetzky Tel Aviv University Media Attached |