Skip to main content

Maximum Satisfiability in Software Analysis: Applications and Techniques

Si, Xujie, Zhang, Xin, Grigore, Radu, Naik, Mayur (2017) Maximum Satisfiability in Software Analysis: Applications and Techniques. In: Lecture Notes in Computer Science. Computer Aided Verification: 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017 Proceedings, Part I. 10426. pp. 68-94. Springer ISBN 978-3-319-63386-2. (doi:10.1007/978-3-319-63387-9_4) (KAR id:63671)

PDF Author's Accepted Manuscript
Language: English
Download (430kB) Preview
Official URL


A central challenge in software analysis concerns balancing different competing tradeoffs. To address this challenge, we propose an approach based on the Maximum Satisfiability (MaxSAT) problem, an optimization extension of the Boolean Satisfiability (SAT) problem. We demonstrate the approach on three diverse applications that advance the state-of-the-art in balancing tradeoffs in software analysis. Enabling these applications on real-world programs necessitates solving large MaxSAT instances comprising over 10301030 clauses in a sound and optimal manner. We propose a general framework that scales to such instances by iteratively expanding a subset of clauses while providing soundness and optimality guarantees. We also present new techniques to instantiate and optimize the framework.

Item Type: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1007/978-3-319-63387-9_4
Divisions: Faculties > Sciences > School of Computing
Depositing User: Radu Grigore
Date Deposited: 29 Sep 2017 08:31 UTC
Last Modified: 29 May 2019 19:36 UTC
Resource URI: (The current URI for this page, for reference purposes)
Grigore, Radu:
  • Depositors only (login required):


Downloads per month over past year