Paper Info
Title
CalCS: SMT solving for non-linear convex constraints
Abstract
Certain formal verification tasks require reasoning about Boolean combinations of non-linear arithmetic constraints over the real numbers. In this paper, we present a new technique for satisfiability solving of Boolean combinations of non-linear constraints that are convex. Our approach applies fundamental results from the theory of convex programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy combination of SAT and a theory solver. A key step in our algorithm is the use of complementary slackness and duality theory to generate succinct infeasibility proofs that support conflict-driven learning. Moreover, whenever non-convex constraints are produced from Boolean reasoning, we provide a procedure that generates conservative approximations of the original set of constraints by using geometric properties of convex sets and supporting hyperplanes. We validate CalCS on several benchmarks including formulas generated from bounded model checking of hybrid automata and static analysis of floating-point software.
Year
Venue
Keywords
2010
FMCAD
boolean combination,convex programming,non-linear arithmetic constraint,boolean reasoning,non-linear constraint,satisfiability modulo theory,bounded model checking,convex set,duality theory,theory solver,non-linear convex constraint,cost accounting,formal verification,programming,floating point,convex functions,optimization,cognition,computability,static analysis,boolean algebra,automata,satisfiability modulo theories,satisfiability
Field
DocType
Citations 
Model checking,Duality (mathematics),Computer science,Theoretical computer science,Computability,Convex function,Boolean algebra,Solver,Convex optimization,Formal verification
Conference
24
PageRank 
References 
Authors
1.10
17
4
Name
Order
Citations
PageRank
Pierluigi Nuzzo130533.35
Alberto Puggelli213210.13
Sanjit A. Seshia32226168.09
Alberto L. Sangiovanni-Vincentelli4113851881.40