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

• 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
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 3353170 (Why is no real title available?)
• Interpolants and Symbolic Model Checking
• Linear temporal logic symbolic model checking
• Model checking
• Symbolic model checking: \(10^{20}\) states and beyond
• Zero-suppressed BDDs and their applications

Cited in

(24)

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

Describes a project that uses

Uses Software

• NuSMV
• CUDD

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)