Formal verification based on Boolean expression diagrams

DOI10.1016/S1571-0661(04)00331-7MaRDI QIDQ1954165zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Boolean expression diagrams
• scientific article; zbMATH DE number 1701749
• scientific article; zbMATH DE number 1670773
• Symbolic model checking: \(10^{20}\) states and beyond
• scientific article; zbMATH DE number 1390338

Cites work

• scientific article; zbMATH DE number 1629965 (Why is no real title available?)
• scientific article; zbMATH DE number 1670773 (Why is no real title available?)
• scientific article; zbMATH DE number 1670796 (Why is no real title available?)
• scientific article; zbMATH DE number 1701749 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1149437 (Why is no real title available?)
• scientific article; zbMATH DE number 1538056 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 2102720 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• scientific article; zbMATH DE number 846270 (Why is no real title available?)
• scientific article; zbMATH DE number 910727 (Why is no real title available?)
• scientific article; zbMATH DE number 1424030 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary Decision Diagrams
• Boolean expression diagrams
• Bypassing BDD construction for reliability analysis
• Efficient Boolean manipulation with OBDD's can be extended to FBDD's
• Formal verification based on Boolean expression diagrams
• GRASP: a search algorithm for propositional satisfiability
• Graph driven BDDs -- a new data structure for Boolean functions
• Graph-Based Algorithms for Boolean Function Manipulation
• Ordered binary decision diagrams and the Davis-Putnam procedure
• Pattern Matching in Trees
• SATO: An efficient propositional prover
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(7)

• scientific article; zbMATH DE number 1670798 (Why is no real title available?)
• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• scientific article; zbMATH DE number 139969 (Why is no real title available?)
• Formal verification based on Boolean expression diagrams
• Boolean expression diagrams
• scientific article; zbMATH DE number 1670773 (Why is no real title available?)
• scientific article; zbMATH DE number 1701749 (Why is no real title available?)

Describes a project that uses

Uses Software

• HANNIBAL
• SATO
• CUDD
• NuSMV

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

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