Maximum Satisfiability in Software Analysis: Applications and Techniques


A central challenge in software analysis concerns balancingdifferent competing tradeoffs. To address this challenge, we proposean 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 advancethe state-of-the-art in balancing tradeoffs in software analysis.Enabling these applications on real-world programs necessitates solvinglarge MaxSAT instances comprising over 1030 clauses in a sound andoptimal manner. We propose a general framework that scales to suchinstances by iteratively expanding a subset of clauses while providingsoundness and optimality guarantees. We also present new techniques toinstantiate and optimize the framework.

In Computer Aided Verification, 29th International Conference