| Publication | Date of Publication | Type |
|---|
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Automated Reasoning | 2022-11-09 | Paper |
scientific article; zbMATH DE number 7566057 (Why is no real title available?)
(available as arXiv preprint) | 2022-08-02 | Paper |
| scientific article; zbMATH DE number 7566057 (Why is no real title available?) | 2022-08-02 | Paper |
| The Lean 4 theorem prover and programming language | 2021-12-01 | Paper |
| scientific article; zbMATH DE number 7178358 (Why is no real title available?) | 2020-03-09 | Paper |
Congruence closure in intensional type theory
Automated Reasoning | 2016-09-05 | Paper |
The Lean theorem prover (system description)
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Cutting to the chase.
Journal of Automated Reasoning | 2015-06-23 | Paper |
A model-constructing satisfiability calculus
Lecture Notes in Computer Science | 2014-11-03 | Paper |
Efficiently solving quantified bit-vector formulas
Formal Methods in System Design | 2014-03-28 | Paper |
Model-based theory combination
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
| Justifying equality | 2013-09-25 | Paper |
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
The strategy challenge in SMT solving
Automated Reasoning and Mathematics | 2013-04-16 | Paper |
Real Algebraic Strategies for MetiTarski Proofs
Lecture Notes in Computer Science | 2012-09-07 | Paper |
Solving non-linear arithmetic
Automated Reasoning | 2012-09-05 | Paper |
On deciding satisfiability by theorem proving with speculative inferences
Journal of Automated Reasoning | 2012-07-31 | Paper |
Cutting to the chase. Solving linear integer arithmetic
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Symbolic automata constraint solving
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Bugs, moles and skeletons: symbolic reasoning for software development
Automated Reasoning | 2010-09-14 | Paper |
Deciding effectively propositional logic using DPLL and substitution sets
Journal of Automated Reasoning | 2010-05-26 | Paper |
Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Satisfiability modulo theories: an appetizer
Lecture Notes in Computer Science | 2009-12-09 | Paper |
On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Computer Aided Verification | 2009-06-30 | Paper |
Efficient E-Matching for SMT Solvers
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
Automated Reasoning | 2008-11-27 | Paper |
Engineering DPLL(T) + Saturation
Automated Reasoning | 2008-11-27 | Paper |
A Tutorial on Satisfiability Modulo Theories
Computer Aided Verification | 2007-11-29 | Paper |
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
Formal Methods in System Design | 2007-11-28 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
Journal of Automated Reasoning | 2007-01-30 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | 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 2090318 (Why is no real title available?) | 2004-08-12 | Paper |
