More Like this

1. CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length

   Bonacina, Maria Paola ; Graham-Lengrand, Stephane ; Shankar, Natarajan ( August 2022 , Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings)

   Deharbe, David ; Hyvarinen, Antti E. (Ed.)

   CDSAT (Conflict-Driven Satisfiability) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length, which is an abstraction of the theory of arrays with length. The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved. 

   more » « less
2. SMC: Satisfiability Modulo Convex Programming

   https://doi.org/10.1109/JPROC.2018.2849003  

   Shoukry, Yasser ; Nuzzo, Pierluigi ; Sangiovanni-Vincentelli, Alberto L. ; Seshia, Sanjit A. ; Pappas, George J. ; Tabuada, Paulo ( January 2018 , Proceedings of the IEEE)

   The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of ``cyber'' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming. 

   more » « less
3. TBUDDY: A Proof-Generating BDD Package

   Bryant, Randal E. ( October 2022 , Formal methods in computeraided design)

   Griggio, Alberto ; Rungta, Neha (Ed.)

   The TBUDDY library enables the construction and manipulation of reduced, ordered binary decision diagrams (BDDs). It extends the capabilities of the BUDDY BDD pack- age to support trusted BDDs, where the generated BDDs are accompanied by proofs of their logical properties. These proofs are expressed in a standard clausal framework, for which a variety of proof checkers are available. Building on TBUDDY via its application-program interface (API) enables developers to implement automated reasoning tools that generate correctness proofs for their outcomes. In some cases, BDDs serve as the core reasoning mechanism for the tool, while in other cases they provide a bridge from the core reasoner to proof generation. A Boolean satisfiability (SAT) solver based on TBUDDY achieves polynomial scaling when generating unsatisfiability proofs for a number of problems that yield exponentially-sized proofs with standard solvers. It performs particularly well for formulas containing parity constraints, where it can employ Gaussian elimination to systematically simplify the constraints. 

   more » « less
4. Clausal Proofs for Pseudo-Boolean Reasoning

   https://doi.org/10.1007/978-3-030-99524-9_25  

   Bryant, Randal E. ; Heule, Marijn J. ( January 2022 , International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   Fisman, D. ; Rosu, G. (Ed.)

   When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs. 

   more » « less
5. Formal Verification of Bit-Vector Invertibility Conditions in Coq

   Ekici, Burak ; Viswanathan, Arjun ; Zohar, Yoni ; Tinelli, Cesare ; Barrett, Clark ( September 2023 , Proceedings of the International Symposium on Frontiers of Combining Systems (FroCoS 2023))

   Sattler, U. ; Suda, M. (Ed.)

   We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors—used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5— in the Coq proof assistant. Previous work proved many of these in a completely automatic fashion for arbitrary bit-width; however, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over larger bit-widths. In this paper we describe the process of proving a representative subset of these invertibility conditions in Coq. In particular, we describe the BVList library for bit-vectors in Coq, our extensions to it, and proofs of the invertibility conditions. 

   more » « less