Structuring abstract interpreters through state and value abstractions - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

Structuring abstract interpreters through state and value abstractions

Résumé

We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be pluggedin. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable 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-C framework. We present the domains that are available so far within eva, and show that this communication mechanism is able to handle them seamlessly.
Fichier non déposé

Dates et versions

cea-01808886 , version 1 (06-06-2018)

Identifiants

Citer

Sandrine Blazy, David Bühler, Boris Yakobowski. Structuring abstract interpreters through state and value abstractions. 18th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI 2017), Jan 2017, Paris, France. pp.112-130, ⟨10.1007/978-3-319-52234-0_7⟩. ⟨cea-01808886⟩
320 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More