BDD-based symbolic model checking

DOI10.1007/978-3-319-10575-8_8zbMATH Open1392.68239OpenAlexW2803843036MaRDI QIDQ3176366FDOQ3176366

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

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

Mathematics Subject Classification ID

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

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• Symbolic model checking: \(10^{20}\) states and beyond
• Title not available (Why is that?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary Decision Diagrams
• Zero-suppressed BDDs and their applications
• Interpolants and Symbolic Model Checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear temporal logic symbolic model checking
• Finiteness is mu-ineffable

Cited In (20)

• Title not available (Why is that?)
• Formal verification of a Java component using the RESOLVE framework
• Formal Methods for Hardware Verification
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Title not available (Why is that?)
• Automatically finding the right probabilities in Bayesian networks
• Title not available (Why is that?)
• Model Checking Procedural Programs
• Theorem Proving in Higher Order Logics
• Combining Model Checking and Deduction
• Binary Decision Diagrams
• Abstraction and Abstraction Refinement
• Title not available (Why is that?)
• Generating BDDs for symbolic model checking in CCS
• Satisfiability Modulo Theories
• 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
• Implementation and Application of Automata
• Title not available (Why is that?)

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)