BDD-based symbolic model checking

DOI10.1007/978-3-319-10575-8_8MaRDI QIDQ3176366zbMATH OpenOpenAlexFDO

Authors Sagar Chaki, Arie Gurfinkel

Publication date 20 July 2018

Published in Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10575-8_8

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2086590
• scientific article; zbMATH DE number 1507203
• scientific article; zbMATH DE number 2086515
• Formal Methods for Hardware Verification
• Symbolic model checking: \(10^{20}\) states and beyond

Cites work

• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• scientific article; zbMATH DE number 3353170 (Why is no real title available?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary Decision Diagrams
• Finiteness is mu-ineffable
• Graph-Based Algorithms for Boolean Function Manipulation
• Interpolants and Symbolic Model Checking
• Linear temporal logic symbolic model checking
• Symbolic model checking: \(10^{20}\) states and beyond
• Zero-suppressed BDDs and their applications

Cited in

(23)

• Implementation and Application of Automata
• scientific article; zbMATH DE number 2086515 (Why is no real title available?)
• Formal verification of a Java component using the RESOLVE framework
• Formal Methods for Hardware Verification
• Model checking procedural programs
• Improving BDD based symbolic model checking with isomorphism exploiting transition relations
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• scientific article; zbMATH DE number 1507203 (Why is no real title available?)
• Binary decision diagrams
• Abstraction and abstraction refinement
• Automatically finding the right probabilities in Bayesian networks
• scientific article; zbMATH DE number 834569 (Why is no real title available?)
• Satisfiability modulo theories
• Theorem Proving in Higher Order Logics
• Combining Model Checking and Deduction
• Model checking technology and tool development based on Groebner base
• scientific article; zbMATH DE number 2086590 (Why is no real title available?)
• Programming a symbolic model checker in a fully expansive theorem prover
• Generating BDDs for symbolic model checking in CCS
• Tools and Algorithms for the Construction and Analysis of Systems
• Formal Verification of Infinite State Systems Using Boolean Methods
• Directed Model Checking for B: An Evaluation and New Techniques
• scientific article; zbMATH DE number 139820 (Why is no real title available?)

Describes a project that uses

Uses Software

• CUDD
• NuSMV

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

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