Formal verification based on Boolean expression diagrams

DOI10.1016/S1571-0661(04)00331-7zbMath1266.68004OpenAlexW1976278643MaRDI QIDQ1954165

Poul Frederick Williams

Publication date: 20 June 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)00331-7

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items (2)

Formal verification based on Boolean expression diagrams ⋮ Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.

Uses Software

• NuSMV
• CUDD
• SATO
• HANNIBAL

Cites Work

• Graph driven BDDs -- a new data structure for Boolean functions
• Symbolic model checking: \(10^{20}\) states and beyond
• Bypassing BDD construction for reliability analysis
• Formal verification based on Boolean expression diagrams
• Boolean expression diagrams
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Pattern Matching in Trees
• Binary Decision Diagrams
• Efficient Boolean manipulation with OBDD's can be extended to FBDD's
• GRASP: a search algorithm for propositional satisfiability
• Ordered Binary Decision Diagrams and the Davis-Putnam procedure
• SATO: An efficient propositional prover
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formal verification based on Boolean expression diagrams