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

DOI10.1007/978-3-540-69850-0_9zbMATH Open1142.68430OpenAlexW1589254173MaRDI QIDQ3512438FDOQ3512438

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

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

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)

Cites Work

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

Cited In (13)

• Scalable error detection using Boolean satisfiability
• Computer Aided Verification
• Formal Methods for Hardware Verification
• Title not available (Why is that?)
• Hybrid BDD and All-SAT Method for Model Checking
• Binary decision diagrams
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An optimized symbolic bounded model checking engine
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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)