| Publication | Date of Publication | Type |
|---|
| Certified knowledge compilation with application to verified model counting | 2024-11-26 | Paper |
| Clausal proofs for pseudo-Boolean reasoning | 2024-01-23 | Paper |
| Moving definition variables in quantified Boolean formulas | 2024-01-23 | Paper |
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
ACM Transactions on Computational Logic | 2023-11-03 | Paper |
Preprocessing of propagation redundant clauses
Journal of Automated Reasoning | 2023-10-24 | Paper |
| Preprocessing of propagation redundant clauses | 2022-12-07 | Paper |
| Dual proof generation for quantified Boolean formulas with a BDD-based solver | 2021-12-01 | Paper |
Generating extended resolution proofs with a BDD-based SAT solver
(available as arXiv preprint) | 2021-08-04 | Paper |
Chain reduction for binary and zero-suppressed decision diagrams
Journal of Automated Reasoning | 2020-11-02 | Paper |
Chain reduction for binary and zero-suppressed decision diagrams
Tools and Algorithms for the Construction and Analysis of Systems | 2019-09-16 | Paper |
On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
IEEE Transactions on Computers | 2018-09-14 | Paper |
Binary decision diagrams
Handbook of Model Checking | 2018-07-20 | Paper |
Predicate abstraction with indexed predicates
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Boolean satisfiability with transitivity constraints
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
A symbolic approach to predicate abstraction.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Deductive verification of advanced out-of-order microprocessors.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Unbounded, fully symbolic model checking of timed automata using Boolean methods.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Convergence testing in term-level bounded model checking
Lecture Notes in Computer Science | 2010-02-05 | Paper |
FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
Lecture Notes in Computer Science | 2009-08-06 | Paper |
State-set branching: leveraging BDDs for heuristic search
Artificial Intelligence | 2009-07-17 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
Formal Verification of Infinite State Systems Using Boolean Methods
Lecture Notes in Computer Science | 2008-09-25 | Paper |
A View from the Engine Room: Computational Support for Symbolic Model Checking
25 Years of Model Checking | 2008-07-15 | Paper |
Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
Logical Methods in Computer Science | 2007-10-11 | Paper |
| On solving Boolean combinations of UTVPI constraints. | 2007-10-09 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Deciding Bit-Vector Arithmetic with Abstraction
Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-03 | Paper |
On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
IEEE Transactions on Computers | 2007-01-09 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
| scientific article; zbMATH DE number 2102727 (Why is no real title available?) | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2102716 (Why is no real title available?) | 2004-09-24 | Paper |
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
Journal of Symbolic Computation | 2004-03-14 | Paper |
| scientific article; zbMATH DE number 1979548 (Why is no real title available?) | 2003-09-14 | Paper |
| scientific article; zbMATH DE number 1903355 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1903346 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1798182 (Why is no real title available?) | 2002-11-04 | Paper |
Verification of arithmetic circuits using binary moment diagrams
International Journal on Software Tools for Technology Transfer. STTT | 2002-07-25 | Paper |
| scientific article; zbMATH DE number 1670770 (Why is no real title available?) | 2001-11-11 | Paper |
Geometric characterization of series-parallel variable resistor networks
IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications | 1997-05-28 | Paper |
A methodology for hardware verification based on logic simulation
Journal of the ACM | 1995-03-30 | Paper |
| scientific article; zbMATH DE number 177501 (Why is no real title available?) | 1993-05-18 | Paper |
| scientific article; zbMATH DE number 177244 (Why is no real title available?) | 1993-05-18 | Paper |
Graph-Based Algorithms for Boolean Function Manipulation
IEEE Transactions on Computers | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 3993458 (Why is no real title available?) | 1986-01-01 | Paper |
A Switch-Level Model and Simulator for MOS Digital Systems
IEEE Transactions on Computers | 1984-01-01 | Paper |
