| Publication | Date of Publication | Type |
|---|
LISA -- a modern proof system
| 2024-11-26 | Paper |
Succinct ordering and aggregation constraints in algebraic array theories
Journal of Logical and Algebraic Methods in Programming | 2024-06-25 | Paper |
On algebraic array theories
Journal of Logical and Algebraic Methods in Programming | 2024-02-12 | Paper |
Equivalence checking for orthocomplemented bisemilattices in log-linear time
| 2024-02-01 | Paper |
Formula normalizations in verification
| 2024-02-01 | Paper |
Orthologic with Axioms
| 2023-07-14 | Paper |
NP satisfiability for arrays as powers
| 2022-07-08 | Paper |
Generalized arrays for Stainless frames
| 2022-07-08 | Paper |
Minimal synthesis of string to string functions from examples
| 2020-01-23 | Paper |
Refutation-based synthesis in SMT
Formal Methods in System Design | 2019-12-18 | Paper |
Counterexample-guided quantifier instantiation for synthesis in SMT
| 2018-03-01 | Paper |
Solving quantified linear arithmetic by counterexample-guided instantiation
Formal Methods in System Design | 2018-01-08 | Paper |
Contract-based resource verification for higher-order functions with memoization
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Translating Scala programs to Isabelle/HOL. System description
Automated Reasoning | 2016-09-05 | Paper |
On recursion-free Horn clauses and Craig interpolation
Formal Methods in System Design | 2015-10-20 | Paper |
Decision procedures for algebraic data types with abstractions
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
Role analysis
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
Induction for SMT solvers
Lecture Notes in Computer Science | 2015-02-04 | Paper |
Reductions for synthesis procedures
Lecture Notes in Computer Science | 2014-11-03 | Paper |
Verifying and synthesizing software with recursive functions (invited contribution)
Automata, Languages, and Programming | 2014-07-01 | Paper |
Sound compilation of reals
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Numerical representations as purely functional data structures
| 2013-06-10 | Paper |
scientific article; zbMATH DE number 6168149 (Why is no real title available?)
| 2013-05-29 | Paper |
Accelerating interpolants
Automated Technology for Verification and Analysis | 2012-11-21 | Paper |
Synthesis for Unbounded Bit-Vector Arithmetic
Automated Reasoning | 2012-09-05 | Paper |
An efficient decision procedure for imperative tree data structures
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Scala to the Power of Z3: Integrating SMT and Programming
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Towards Complete Reasoning about Axiomatic Specifications
Lecture Notes in Computer Science | 2011-02-15 | Paper |
Sets with cardinality constraints in satisfiability modulo theories
Lecture Notes in Computer Science | 2011-02-15 | Paper |
MUNCH -- automated reasoner for sets and multisets
Automated Reasoning | 2010-09-14 | Paper |
Ordered sets in the calculus of data structures
Computer Science Logic | 2010-09-03 | Paper |
Building a calculus of data structures
Lecture Notes in Computer Science | 2010-01-14 | Paper |
Collections, Cardinalities, and Relations
Lecture Notes in Computer Science | 2010-01-14 | Paper |
Combining theories with shared set operations
Frontiers of Combining Systems | 2010-01-07 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
Automated Deduction – CADE-21 | 2009-03-06 | Paper |
Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
Computer Science Logic | 2008-11-20 | Paper |
Linear Arithmetic with Stars
Computer Aided Verification | 2008-07-15 | Paper |
Using First-Order Theorem Provers in the Jahob Data Structure Verification System
Lecture Notes in Computer Science | 2008-04-04 | Paper |
Decision Procedures for Multisets with Cardinality Constraints
Lecture Notes in Computer Science | 2008-04-04 | Paper |
Runtime Checking for Separation Logic
Lecture Notes in Computer Science | 2008-04-04 | Paper |
Polynomial Constraints for Sets with Cardinality Bounds
Foundations of Software Science and Computational Structures | 2007-09-07 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Deciding Boolean algebra with Presburger arithmetic
Journal of Automated Reasoning | 2007-01-30 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2005-12-06 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2005-08-24 | Paper |
scientific article; zbMATH DE number 2090860 (Why is no real title available?)
| 2004-08-13 | Paper |
scientific article; zbMATH DE number 2044492 (Why is no real title available?)
| 2004-02-18 | Paper |
scientific article; zbMATH DE number 1975601 (Why is no real title available?)
| 2003-09-07 | Paper |
scientific article; zbMATH DE number 1868923 (Why is no real title available?)
| 2003-02-16 | Paper |
scientific article; zbMATH DE number 1805762 (Why is no real title available?)
| 2002-09-24 | Paper |
