Symbolic reachability analysis based on SAT-solvers

DOI10.1007/3-540-46419-0_28MaRDI QIDQ2729082zbMATH OpenFDO

Authors Per Bjesse, Niklas Eén, Parosh A. Abdulla

Publication date 6 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46419-0_28

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 2087634
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• Formal Methods in Computer-Aided Design
• scientific article; zbMATH DE number 2086590
• scientific article; zbMATH DE number 1903357

Cited in

(42)

• Formal verification based on Boolean expression diagrams
• Static analysis and stochastic search for reachability problem
• A Boolean satisfiability approach to the resource-constrained project scheduling problem
• A taxonomy of exact methods for partial Max-SAT
• Symbolic backward reachability with effectively propositional logic. Application to security policy analysis
• Exploiting the real power of unit propagation lookahead
• Towards an efficient library for SAT: A manifesto
• scientific article; zbMATH DE number 1670743 (Why is no real title available?)
• scientific article; zbMATH DE number 1670766 (Why is no real title available?)
• scientific article; zbMATH DE number 1670790 (Why is no real title available?)
• Analysis of Boomerang Differential Trails via a SAT-Based Constraint Solver URSA
• Exploiting target enlargement and dynamic abstraction within mixed BDD and SAT invariant checking
• Interpolant learning and reuse in SAT-based model checking
• SAT-Based Synthesis Methods for Safety Specs
• SAT-Based Model Checking
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• Approximate Symbolic Reachability of Networks of Transition Systems
• A SAT-based technique to analyse networks of finite automata
• Improved SAT-based reachability analysis with observability don't cares
• Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
• Hybrid BDD and All-SAT Method for Model Checking
• New Encodings of Pseudo-Boolean Constraints into CNF
• scientific article; zbMATH DE number 2080057 (Why is no real title available?)
• scientific article; zbMATH DE number 1798189 (Why is no real title available?)
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• scientific article; zbMATH DE number 2086590 (Why is no real title available?)
• scientific article; zbMATH DE number 2087634 (Why is no real title available?)
• Quantifier elimination by dependency sequents
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• A new algorithm for partitioned symbolic reachability analysis
• SAT-Based Analysis of Cellular Automata
• Automated Technology for Verification and Analysis
• Formal Methods in Computer-Aided Design
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• Correct Hardware Design and Verification Methods
• Theory and Applications of Satisfiability Testing
• Tools and Algorithms for the Construction and Analysis of Systems
• A decision diagram operation for reachability
• Weak, strong, and strong cyclic planning via symbolic model checking
• Symbolic techniques in satisfiability solving

Describes a project that uses

Uses Software

• SATO

This page was built for publication: Symbolic reachability analysis based on SAT-solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2729082)