@inbook{307e3c4e8ae547c89618d675ee9ef782,
title = "2-Pointer Logic",
abstract = "For reasoning about properties of pointers, we consider conjunctions of equalities and dis-equalities between terms built up from address constants by addition of offsets and dereferencing. We call the resulting class of formulas 2-pointer logic. We introduce a quantitative version of congruence closure to provide polynomial time algorithms for deciding satisfiability as well as implication between formulas. By generalizing quantitative congruence closure to quantitative finite automata, we succeed in constructing canonical normal forms so that checking of equivalence between conjunctions reduces to syntactic equality. We apply our techniques to realize abstract transformers for dedicated forms of assignments via pointers, in particular, indefinite, definite and locally invertible assignments. Quantitative finite automata here allow us to restrict formulas to properties expressible by some subterm-closed subset of terms only.",
keywords = "2-pointer logic, abstract transformers for assignments, polynomial normal form, quantitative congruence closure, quantitative equalities and dis-equalities",
author = "Helmut Seidl and Julian Erhard and Michael Schwarz and Sarah Tilscher",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.",
year = "2024",
doi = "10.1007/978-3-031-56222-8\_16",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "281--307",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}