An abstract domain of uninterpreted functions

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

9 Citations (Scopus)


We revisit relational static analysis of numeric variables. Such analyses face two difficulties. First, even inexpensive relational domains scale too poorly to be practical for large code-bases. Second, to remain tractable they have extremely coarse handling of non-linear relations. In this paper, we introduce the subterm domain, a weakly relational abstract domain for inferring equivalences amongst sub- expressions, based on the theory of uninterpreted functions. This pro- vides an extremely cheap approach for enriching non-relational domains with relational information, and enhances precision of both relational and non-relational domains in the presence of non-linear operations. We evaluate the idea in the context of the software verification tool Sea Horn.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
Subtitle of host publication17th International Conference, VMCAI 2016 St. Petersburg, FL, USA, January 17–19, 2016 Proceedings
EditorsBarbara Jobstmann, K. Rustan M. Leino
Place of PublicationBerlin Germany
Number of pages19
ISBN (Electronic)9783662491225
ISBN (Print)9783662491218
Publication statusPublished - 2016
Externally publishedYes
EventVerification, Model Checking and Abstract Interpretation 2016 - St. Petersburg, United States of America
Duration: 17 Jan 201619 Jan 2016
Conference number: 17th

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceVerification, Model Checking and Abstract Interpretation 2016
Abbreviated titleVMCAI 2016
CountryUnited States of America
CitySt. Petersburg
Internet address

Cite this