Using BDDs with combinations of theories

DOI10.1007/3-540-36078-6_13MaRDI QIDQ4428300zbMATH OpenFDO

Authors Pascal Fontaine, E. Pascal Gribomont

Publication date 15 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2514/25140190.htm

Mathematics Subject Classification ID

Classical propositional logic (03B05) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Equational binary decision diagrams
• Bddl: A Type System for Binary Decision Diagrams
• Binary decision diagrams for first-order predicate logic.
• Extending existential quantification in conjuctions of BDDs
• scientific article; zbMATH DE number 2090285

Cited in

(13)

• NP-completeness of small conflict set generation for congruence closure
• Zero, successor and equality in BDDs
• Strategies for combining decision procedures
• NuMDG: a new tool for multiway decision graphs construction
• Salsa: Combining constraint solvers with BDDs for automatic invariant checking
• Equational binary decision diagrams
• Exploiting target enlargement and dynamic abstraction within mixed BDD and SAT invariant checking
• Extending existential quantification in conjuctions of BDDs
• scientific article; zbMATH DE number 2090285 (Why is no real title available?)
• scientific article; zbMATH DE number 834569 (Why is no real title available?)
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• A term rewriting technique for decision graphs
• Explaining control policies through predicate decision diagrams

This page was built for publication: Using BDDs with combinations of theories

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