Publication | Date of Publication | Type |
---|
On algebraic array theories | 2024-02-12 | 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 | 2019-12-18 | Paper |
Counterexample-guided quantifier instantiation for synthesis in SMT | 2018-03-01 | Paper |
Solving quantified linear arithmetic by counterexample-guided instantiation | 2018-01-08 | Paper |
Contract-based resource verification for higher-order functions with memoization | 2017-10-20 | Paper |
Translating Scala Programs to Isabelle/HOL | 2016-09-05 | Paper |
On recursion-free Horn clauses and Craig interpolation | 2015-10-20 | Paper |
Decision procedures for algebraic data types with abstractions | 2015-06-11 | Paper |
Role analysis | 2015-03-17 | Paper |
Induction for SMT Solvers | 2015-02-04 | Paper |
Reductions for Synthesis Procedures | 2014-11-03 | Paper |
Verifying and Synthesizing Software with Recursive Functions | 2014-07-01 | Paper |
Sound compilation of reals | 2014-04-10 | Paper |
https://portal.mardi4nfdi.de/entity/Q4924969 | 2013-06-10 | Paper |
https://portal.mardi4nfdi.de/entity/Q4922308 | 2013-05-29 | Paper |
Accelerating Interpolants | 2012-11-21 | Paper |
Synthesis for Unbounded Bit-Vector Arithmetic | 2012-09-05 | Paper |
Scala to the Power of Z3: Integrating SMT and Programming | 2011-07-29 | Paper |
An Efficient Decision Procedure for Imperative Tree Data Structures | 2011-07-29 | Paper |
Towards Complete Reasoning about Axiomatic Specifications | 2011-02-15 | Paper |
Sets with Cardinality Constraints in Satisfiability Modulo Theories | 2011-02-15 | Paper |
MUNCH - Automated Reasoner for Sets and Multisets | 2010-09-14 | Paper |
Ordered Sets in the Calculus of Data Structures | 2010-09-03 | Paper |
Building a Calculus of Data Structures | 2010-01-14 | Paper |
Collections, Cardinalities, and Relations | 2010-01-14 | Paper |
Combining Theories with Shared Set Operations | 2010-01-07 | Paper |
Verification, Model Checking, and Abstract Interpretation | 2009-05-15 | Paper |
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic | 2009-03-06 | Paper |
Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars | 2008-11-20 | Paper |
Linear Arithmetic with Stars | 2008-07-15 | Paper |
Using First-Order Theorem Provers in the Jahob Data Structure Verification System | 2008-04-04 | Paper |
Runtime Checking for Separation Logic | 2008-04-04 | Paper |
Decision Procedures for Multisets with Cardinality Constraints | 2008-04-04 | Paper |
Polynomial Constraints for Sets with Cardinality Bounds | 2007-09-07 | Paper |
Verification, Model Checking, and Abstract Interpretation | 2007-02-12 | Paper |
Deciding Boolean algebra with Presburger arithmetic | 2007-01-30 | Paper |
Automated Deduction – CADE-20 | 2006-11-01 | Paper |
Verification, Model Checking, and Abstract Interpretation | 2005-12-06 | Paper |
Static Analysis | 2005-08-24 | Paper |
https://portal.mardi4nfdi.de/entity/Q4813414 | 2004-08-13 | Paper |
https://portal.mardi4nfdi.de/entity/Q4448356 | 2004-02-18 | Paper |
https://portal.mardi4nfdi.de/entity/Q4424843 | 2003-09-07 | Paper |
https://portal.mardi4nfdi.de/entity/Q4794072 | 2003-02-16 | Paper |
https://portal.mardi4nfdi.de/entity/Q3148997 | 2002-09-24 | Paper |