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

DOI10.1007/978-3-540-69850-0_9MaRDI QIDQ3512438zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 1629965
• scientific article; zbMATH DE number 2087634
• Bounded model checking using satisfiability solving
• scientific article; zbMATH DE number 1670773
• scientific article; zbMATH DE number 2086590

Cites work

• scientific article; zbMATH DE number 1507203 (Why is no real title available?)
• A machine program for theorem-proving
• Applications of SAT Solvers to Cryptanalysis of Hash Functions
• Bounded model checking using satisfiability solving
• Counterexample-guided abstraction refinement for symbolic model checking
• GRASP: a search algorithm for propositional satisfiability
• Graph-Based Algorithms for Boolean Function Manipulation
• Interpolation and SAT-based model checking.
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• Theory and Applications of Satisfiability Testing

Cited in

(13)

• Scalable error detection using Boolean satisfiability
• Computer Aided Verification
• Formal Methods for Hardware Verification
• scientific article; zbMATH DE number 1903357 (Why is no real title available?)
• Hybrid BDD and All-SAT Method for Model Checking
• Binary decision diagrams
• scientific article; zbMATH DE number 1629965 (Why is no real title available?)
• scientific article; zbMATH DE number 1670773 (Why is no real title available?)
• scientific article; zbMATH DE number 1701750 (Why is no real title available?)
• An optimized symbolic bounded model checking engine
• scientific article; zbMATH DE number 1982200 (Why is no real title available?)
• scientific article; zbMATH DE number 2086590 (Why is no real title available?)
• scientific article; zbMATH DE number 1670555 (Why is no real title available?)

This page was built for publication: A View from the Engine Room: Computational Support for Symbolic Model Checking

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