Donut domains: Efficient non-convex domains for abstract interpretation

Khalil Ghorbal, Franjo Ivančić, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

Abstract

Program analysis using abstract interpretation has been successfully applied in practice to find runtime bugs or prove software correct. Most abstract domains that are used widely rely on convexity for their scalability. However, the ability to express non-convex properties is sometimes required in order to achieve a precise analysis of some numerical properties. This work combines already known abstract domains in a novel way in order to design new abstract domains that tackle some non-convex invariants. The abstract objects of interest are encoded as a pair of two convex abstract objects: the first abstract object defines an over-approximation of the possible reached values, as is done customarily. The second abstract object under-approximates the set of impossible values within the state-space of the first abstract object. Therefore, the geometrical concretization of our objects is defined by a convex set minus another convex set (or hole). We thus call these domains donut domains.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
Pages235-250
Number of pages16
DOIs
StatePublished - Jan 30 2012
Externally publishedYes
Event13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012 - Philadelphia, PA, United States
Duration: Jan 22 2012Jan 24 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7148 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
CountryUnited States
CityPhiladelphia, PA
Period1/22/121/24/12

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Donut domains: Efficient non-convex domains for abstract interpretation'. Together they form a unique fingerprint.

  • Cite this

    Ghorbal, K., Ivančić, F., Balakrishnan, G., Maeda, N., & Gupta, A. (2012). Donut domains: Efficient non-convex domains for abstract interpretation. In Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings (pp. 235-250). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7148 LNCS). https://doi.org/10.1007/978-3-642-27940-9_16