SAT-Based Synthesis Methods for Safety Specs
From MaRDI portal
Abstract: Automatic synthesis of hardware components from declarative specifications is an ambitious endeavor in computer aided design. Existing synthesis algorithms are often implemented with Binary Decision Diagrams (BDDs), inheriting their scalability limitations. Instead of BDDs, we propose several new methods to synthesize finite-state systems from safety specifications using decision procedures for the satisfiability of quantified and unquantified Boolean formulas (SAT-, QBF- and EPR-solvers). The presented approaches are based on computational learning, templates, or reduction to first-order logic. We also present an efficient parallelization, and optimizations to utilize reachability information and incremental solving. Finally, we compare all methods in an extensive case study. Our new methods outperform BDDs and other existing work on some classes of benchmarks, and our parallelization achieves a super-linear speedup. This is an extended version of [5], featuring an additional appendix.
Recommendations
- Hardware and Software, Verification and Testing
- Automated Technology for Verification and Analysis
- Parameterized synthesis with safety properties
- SAT-based induction for temporal safety properties
- Formalizing Dangerous SAT Encodings
- A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis
- Formal Techniques for Networked and Distributed Systems - FORTE 2005
- scientific article; zbMATH DE number 1629965
Cited in
(31)- Boolean functional synthesis: hardness and practical algorithms
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Certified DQBF solving by definition extraction
- DQBDD: an efficient BDD-based DQBF solver
- Solving dependency quantified Boolean formulas using quantifier localization
- Indecision and delays are the parents of failure -- taming them algorithmically by synthesizing delay-resilient control
- Syntax-guided synthesis for lemma generation in hardware model checking
- A symbolic algorithm for lazy synthesis of eager strategies
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Solution validation and extraction for QBF preprocessing
- Long-distance Q-resolution with dependency schemes
- Dependency schemes for DQBF
- Long distance Q-resolution with dependency schemes
- Symbolic system synthesis using answer set programming
- The QBF Gallery: behind the scenes
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs
- Encodings of bounded synthesis
- Solving QBF by abstraction
- A Revised Concept of Safety for General Answer Set Programs
- scientific article; zbMATH DE number 1107560 (Why is no real title available?)
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Size, cost and capacity: a semantic technique for hard random QBFs
- The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Tableaux for realizability of safety specifications
- Synthesis of compact strategies for coordination programs
- Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
- Strategy extraction by interpolation
- Models and counter-models of quantified Boolean formulas (invited talk)
- Synchronous counting and computational algorithm design
This page was built for publication: SAT-Based Synthesis Methods for Safety Specs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938057)
