Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking
Abstract elided by the publisher.
Related papers
- sfHornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses CAV 2025
- Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking CAV 2000
- BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems TACAS 2000
- Optimizing Symbolic Model Checking for Constraint-Rich Models CAV 1999
- Clausal Proofs for Pseudo-Boolean Reasoning TACAS 2022
- Automating Induction for Solving Horn Clauses CAV 2017
- BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability TACAS 2026
- An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs ESOP 2016