| Publication | Date of Publication | Type |
|---|
CoProver: a recommender system for proof construction
Lecture Notes in Computer Science | 2024-02-28 | Paper |
An augmented MetiTarski dataset for real quantifier elimination using machine learning
Lecture Notes in Computer Science | 2024-02-28 | Paper |
Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
Journal of Automated Reasoning | 2022-03-25 | Paper |
The Verified Software Initiative: A Manifesto
Theories of Programming | 2022-02-14 | Paper |
| The correctness of a code generator for a functional language | 2020-08-05 | Paper |
Conflict-driven satisfiability for theory combination: transition system and completeness
Journal of Automated Reasoning | 2020-03-03 | Paper |
TeLEx: learning signal temporal logic from positive examples using tightness metric
Formal Methods in System Design | 2019-11-25 | Paper |
Automated deduction for verification
ACM Computing Surveys | 2019-08-09 | Paper |
The verified software initiative
ACM Computing Surveys | 2019-08-09 | Paper |
On Shostak's decision procedure for combinations of theories
Automated Deduction — Cade-13 | 2019-01-15 | Paper |
| Duality-based nested controller synthesis from STL specifications for stochastic linear systems | 2018-12-06 | Paper |
Combining Model Checking and Deduction
Handbook of Model Checking | 2018-07-20 | Paper |
| Satisfiability modulo theories and assignments | 2017-09-22 | Paper |
| Identifying negative cost cycles in strongly polynomial space | 2016-07-20 | Paper |
The mechanical verification of a DPLL-based satisfiability solver
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
The semantics of Datalog for the evidential tool bus (extended abstract)
Specification, Algebra, and Software | 2014-03-25 | Paper |
| Justifying equality | 2013-09-25 | Paper |
Automated reasoning, fast and slow
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
A mechanical verification of the stressing algorithm for negative cost cycle detection in networks
Science of Computer Programming | 2011-05-04 | Paper |
Rewriting, inference, and proof
Rewriting Logic and Its Applications | 2010-10-12 | Paper |
Unraveling a card trick
Time for Verification | 2010-09-07 | Paper |
Beyond satisfiability: extensions and applications
Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems | 2010-06-02 | Paper |
Fixpoints and search in PVS
Lecture Notes in Computer Science | 2010-05-11 | Paper |
Formal Methods at the Crossroads. From Panacea to Foundational Support
Lecture Notes in Computer Science | 2010-03-30 | Paper |
A Brief Overview of PVS
Lecture Notes in Computer Science | 2008-12-04 | Paper |
A Tutorial on Satisfiability Modulo Theories
Computer Aided Verification | 2007-11-29 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
Lecture Notes in Computer Science | 2006-11-14 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
| scientific article; zbMATH DE number 2102725 (Why is no real title available?) | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2090127 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2090312 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2090060 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2090113 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 1863374 (Why is no real title available?) | 2003-02-04 | Paper |
| scientific article; zbMATH DE number 1759597 (Why is no real title available?) | 2002-11-28 | Paper |
| scientific article; zbMATH DE number 1798183 (Why is no real title available?) | 2002-11-04 | Paper |
| scientific article; zbMATH DE number 1701754 (Why is no real title available?) | 2002-02-05 | Paper |
| scientific article; zbMATH DE number 1670517 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1617290 (Why is no real title available?) | 2001-07-11 | Paper |
A finite element method for electrostrictive ceramic devices
International Journal of Solids and Structures | 1999-08-22 | Paper |
| scientific article; zbMATH DE number 1163987 (Why is no real title available?) | 1998-11-01 | Paper |
| scientific article; zbMATH DE number 1088222 (Why is no real title available?) | 1997-11-17 | Paper |
| Metamathematics, Machines and Gödel's Proof | 1994-06-23 | Paper |
Linearizing intuitionistic implication
Annals of Pure and Applied Logic | 1993-05-16 | Paper |
Decision problems for propositional linear logic
Annals of Pure and Applied Logic | 1992-09-27 | Paper |
