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
• Satisfiability checking using Boolean expression diagrams
• Combining decision diagrams and SAT procedures for efficient symbolic model checking
• Symbolic model checking: \(10^{20}\) states and beyond
• scientific article; zbMATH DE number 1390338

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Applying the Davis-Putnam procedure to non-clausal formulas
• Automatic verification of combinatorial and pipelined FFT circuits
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Binary Decision Diagrams
• Boolean expression diagrams
• Bypassing BDD construction for reliability analysis
• Combining decision diagrams and SAT procedures for efficient symbolic model checking
• Difference decision diagrams
• Efficient Boolean manipulation with OBDD's can be extended to FBDD's
• Formal verification based on Boolean expression diagrams
• Graph driven BDDs -- a new data structure for Boolean functions
• Graph-Based Algorithms for Boolean Function Manipulation
• GRASP: a search algorithm for propositional satisfiability
• 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 846270 (Why is no real title available?)
• scientific article; zbMATH DE number 910727 (Why is no real title available?)
• NuSMV: A new symbolic model verifier
• Ordered binary decision diagrams and the Davis-Putnam procedure
• Pattern Matching in Trees
• Satisfiability checking using Boolean expression diagrams
• SATO: An efficient propositional prover
• Symbolic model checking: \(10^{20}\) states and beyond
• Symbolic reachability analysis based on SAT-solvers
• Tuning SAT checkers for bounded model checking
• Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs

Cited in

(7)

• Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
• Formal verification based on Boolean expression diagrams
• Boolean expression diagrams
• Combining decision diagrams and SAT procedures for efficient symbolic model checking
• Verification diagrams revisited: Disjunctive invariants for easy verification
• Satisfiability checking using Boolean expression diagrams
• scientific article; zbMATH DE number 139969 (Why is no real title available?)

Describes a project that uses

Uses Software

• CUDD
• SATO
• HANNIBAL
• 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)