Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Alain Monteil <>
Submitted on : Thursday, January 14, 2016 - 4:07:49 PM
Last modification on : Thursday, July 1, 2021 - 5:58:08 PM




Arlen Cox, Bor-Yuh Evan Chang, Huisong Li, Xavier Rival. Abstract Domains and Solvers for Sets Reasoning. 20th International Conference, LPAR-20, Nov 2015, Suva, Fiji. ⟨10.1007/978-3-662-48899-7_25⟩. ⟨hal-01256309⟩



Record views