Abstract Domains and Solvers for Sets Reasoning

Abstract : When constructing complex program analyses, it is often useful to reason about not just individual values, but collections of values. Symbolic set abstractions provide building blocks that can be used to partition elements, relate partitions to other partitions, and determine the provenance of multiple values, all without knowing any concrete values. To address the simultaneous challenges of scalability and precision, we formalize and implement an interface for symbolic set abstractions and construct multiple abstract domains relying on both specialized data structures and off-the-shelf theorem provers. We develop techniques for lifting existing domains to improve performance and precision. We evaluate these domains on real-world data structure analysis problems.
Type de document :
Communication dans un congrès
Martin Davis; Ansgar Fehnker; Annabelle McIver; Andrei Voronkov. 20th International Conference, , Nov 2015, Suva, Fiji. Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, Lecture Notes in Computer Science (9450), 〈10.1007/978-3-662-48899-7_25〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01256309
Contributeur : Alain Monteil <>
Soumis le : jeudi 14 janvier 2016 - 16:07:49
Dernière modification le : jeudi 11 janvier 2018 - 06:25:39

Identifiants

Collections

Citation

Arlen Cox, Bor-Yuh Evan Chang, Huisong Li, Xavier Rival. Abstract Domains and Solvers for Sets Reasoning. Martin Davis; Ansgar Fehnker; Annabelle McIver; Andrei Voronkov. 20th International Conference, , Nov 2015, Suva, Fiji. Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, Lecture Notes in Computer Science (9450), 〈10.1007/978-3-662-48899-7_25〉. 〈hal-01256309〉

Partager

Métriques

Consultations de la notice

230