CalCS
CalCS: SMT solving for non-linear convex constraints. 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.
This software is also peer reviewed by journal TOMS.
This software is also peer reviewed by journal TOMS.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
Sorted by year (- Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
- Navarro-López, E. M.; O’Toole, M. D.: Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties (2018)
- Roux, Pierre; Iguernlala, Mohamed; Conchon, Sylvain: A non-linear arithmetic procedure for control-command software verification (2018)
- Roux, Pierre; Voronin, Yuen-Lam; Sankaranarayanan, Sriram: Validating numerical semidefinite programming solvers for polynomial invariants (2018)
- Cimatti, Alessandro; Griggio, Alberto; Irfan, Ahmed; Roveri, Marco; Sebastiani, Roberto: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF (2017)
- Shoukry, Yasser; Nuzzo, Pierluigi; Sangiovanni-Vincentelli, Alberto L.; Seshia, Sanjit A.; Pappas, George J.; Tabuada, Paulo: SMC: satisfiability modulo convex optimization (2017)
- Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Minimal-model-guided approaches to solving polynomial constraints and extensions (2014)
- Gao, Sicun; Kong, Soonho; Clarke, Edmund M.: dReal: an SMT solver for nonlinear theories over the reals (2013)