This paper proposes a new approach for deriving invariants that are systems of congruence equations where the modulo is a power of 2. The technique is an amalgam of SAT-solving, where a propositional formula is used to encode the semantics of a basic block, and abstraction, where the solutions to the formula are systematically combined and summarised as a system of congruence equations. The resulting technique is more precise than existing congruence analyses since a single optimal transfer function is derived for a basic block as a whole. © 2008 Springer-Verlag.
CITATION STYLE
King, A., & Søndergaard, H. (2008). Inferring congruence equations using SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 281–293). https://doi.org/10.1007/978-3-540-70545-1_26
Mendeley helps you to discover research relevant for your work.