A View from the Engine Room: Computational Support for Symbolic Model Checking

DOI10.1007/978-3-540-69850-0_9zbMath1142.68430OpenAlexW1589254173MaRDI QIDQ3512438

Randal E. Bryant

Publication date: 15 July 2008

Published in: 25 Years of Model Checking (Search for Journal in Brave)

Full work available at URL: https://figshare.com/articles/journal_contribution/A_View_from_the_Engine_Room_Computational_Support_for_Symbolic_Model_Checking/6602861

zbMATH Keywords

satisfiabilitybinary decision diagramscapabilities of SAT solvers and BDD packagesfuture perspectives of model checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Binary Decision Diagrams

Cites Work

• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Counterexample-guided abstraction refinement for symbolic model checking
• Graph-Based Algorithms for Boolean Function Manipulation
• GRASP: a search algorithm for propositional satisfiability
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• Applications of SAT Solvers to Cryptanalysis of Hash Functions
• Computer Aided Verification
• Bounded model checking using satisfiability solving
• Unnamed Item