An abstract domain of uninterpreted functions

G Gange; J Navas Laserna; P Schachte; H SONDERGAARD; P Stuckey

Conference Proceedings

An abstract domain of uninterpreted functions

G Gange, J Navas Laserna, P Schachte, H SONDERGAARD, P Stuckey, B Jobstmann (ed.), KRM Leino (ed.)

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Springer Berlin Heidelberg | Published : 2016

DOI: 10.1007/978-3-662-49122-5

Abstract

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 evaluat..

View full abstract