Integrating BDD-based and SAT-based symbolic model checking

DOI10.1007/3-540-45988-X_5MaRDI QIDQ4737124zbMATH OpenFDO

Authors Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella

Publication date 11 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2309/23090049.htm, https://hdl.handle.net/11572/358375

Mathematics Subject Classification ID

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

Recommendations

• BDD-based symbolic model checking
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• Symbolic reachability analysis based on SAT-solvers
• Industrial model checking based on satisfiability solvers
• Applying SAT methods in unbounded symbolic model checking

Cited in

(10)

• NuSMV: A new symbolic model checker
• Generating BDDs for symbolic model checking in CCS
• Symbolic reachability analysis based on SAT-solvers
• Towards deriving test sequences by model checking
• BDD-based symbolic model checking
• A View from the Engine Room: Computational Support for Symbolic Model Checking
• Hybrid BDD and All-SAT Method for Model Checking
• NuSMV 2: An OpenSource tool for symbolic model checking
• Weak, strong, and strong cyclic planning via symbolic model checking
• Conformant planning via symbolic model checking and heuristic search

Describes a project that uses

Uses Software

• SPIN
• Chaff
• CUDD
• NuSMV

This page was built for publication: Integrating BDD-based and SAT-based symbolic model checking

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