BDD-Based Symbolic Model Checking

DOI10.1007/978-3-319-10575-8_8zbMath1392.68239OpenAlexW2803843036MaRDI QIDQ3176366

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

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

Related Items (6)

Formal verification of a Java component using the RESOLVE framework ⋮ Binary Decision Diagrams ⋮ Satisfiability Modulo Theories ⋮ Abstraction and Abstraction Refinement ⋮ Model Checking Procedural Programs ⋮ Combining Model Checking and Deduction

Uses Software

• NuSMV
• CUDD

Cites Work

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

This page was built for publication: BDD-Based Symbolic Model Checking