[ACM Press the 41st ACM SIGPLAN-SIGACT Symposium - San Diego, California, USA (2014.01.22-2014.01.24)] Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '14 - Abstract satisfaction

✍ Scribed by D'Silva, Vijay; Haller, Leopold; Kroening, Daniel

• Book ID: 121855809
• Publisher: ACM Press
• Year: 2014
• Weight: 694 KB
• Category: Article
• ISBN: 1450325440
• DOI: 10.1145/2535838.2535868

✦ Synopsis

This article introduces an abstract interpretation framework that codifies the operations in SAT and SMT solvers in terms of lattices, transformers and fixed points. We develop the idea that a formula denotes a set of models in a universe of structures. This set of models has characterizations as fixed points of deduction, abduction and quantification transformers. A wide range of satisfiability procedures can be understood as computing and refining approximations of such fixed points. These include procedures in the DPLL family, those for preprocessing and inprocessing in SAT solvers, decision procedures for equality logics, weak arithmetics, and procedures for approximate quantification. Our framework provides a unified, mathematical basis for studying and combining program analysis and satisfiability procedures. A practical benefit of our work is a new, logic-agnostic architecture for implementing solvers.