| Publication | Date of Publication | Type |
|---|
| Theorem proving modulo associativity | 2024-06-21 | Paper |
Constrained dynamic partial order reduction
Computer Aided Verification | 2023-05-05 | Paper |
A precedence-based total AC-compatible ordering
Rewriting Techniques and Applications | 2022-12-09 | Paper |
A recursive path ordering for higher-order terms in η-long β-normal form
Rewriting Techniques and Applications | 2022-12-09 | Paper |
| Using automated reasoning techniques for enhancing the efficiency and security of (Ethereum) smart contracts | 2022-12-07 | Paper |
| Distilling Constraints in Zero-Knowledge Protocols | 2022-12-07 | Paper |
| Lower-bound synthesis using loop specialization and Max-SMT | 2022-03-25 | Paper |
| SDN-actors: modeling and verification of SDN programs | 2021-05-04 | Paper |
Actor-based model checking for software-defined networks
Journal of Logical and Algebraic Methods in Programming | 2021-02-26 | Paper |
Actor-based model checking for software-defined networks
Journal of Logical and Algebraic Methods in Programming | 2021-02-26 | Paper |
Proving termination through conditional termination
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Resource analysis driven by (conditional) termination proofs
Theory and Practice of Logic Programming | 2020-05-04 | Paper |
AC-superposition with constraints: no AC-unifiers needed
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Incomplete SMT techniques for solving non-linear formulas over the integers
ACM Transactions on Computational Logic | 2019-11-22 | Paper |
Extension orderings
Automata, Languages and Programming | 2019-01-10 | Paper |
Speeding up the constraint-based method in difference logic
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Termination Competition (termCOMP 2015)
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
The computability path ordering
Logical Methods in Computer Science | 2015-10-29 | Paper |
Normal higher-order termination
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
SMT-based array invariant generation
Lecture Notes in Computer Science | 2014-11-03 | Paper |
Minimal-model-guided approaches to solving polynomial constraints and extensions
Lecture Notes in Computer Science | 2014-09-26 | Paper |
Paramodulation with non-monotonic orderings and simplification
Journal of Automated Reasoning | 2013-07-05 | Paper |
The recursive path and polynomial ordering for first-order and higher-order terms
Journal Of Logic And Computation | 2013-04-19 | Paper |
Nominal completion for rewrite systems with binders
Automata, Languages, and Programming | 2012-11-01 | Paper |
SAT modulo linear arithmetic for solving polynomial constraints
Journal of Automated Reasoning | 2012-07-31 | Paper |
A Monotonic Higher-Order Semantic Path Ordering
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-05-06 | Paper |
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Paramodulation with Well-founded Orderings
Journal Of Logic And Computation | 2009-04-16 | Paper |
Orderings and Constraints: Theory and Practice of Proving Termination
Rewriting, Computation and Proof | 2009-03-06 | Paper |
Polymorphic higher-order recursive path orderings
Journal of the ACM | 2008-12-21 | Paper |
The Computability Path Ordering: The End of a Quest
Computer Science Logic | 2008-11-20 | Paper |
Higher-Order Orderings for Normal Rewriting
Lecture Notes in Computer Science | 2008-09-25 | Paper |
Higher-Order Termination: From Kruskal to Computability
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Recursive Path Orderings Can Also Be Incremental
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
HORPO with Computability Closure: A Reconstruction
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
Challenges in Satisfiability Modulo Theories
Lecture Notes in Computer Science | 2008-01-02 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Term Rewriting and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
| scientific article; zbMATH DE number 2090319 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2090310 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2043535 (Why is no real title available?) | 2004-02-16 | Paper |
Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
Journal of Automated Reasoning | 2003-06-09 | Paper |
| Paramodulation-based theorem proving | 2002-08-27 | Paper |
A fully syntactic AC-RPO.
Information and Computation | 2002-01-01 | Paper |
| scientific article; zbMATH DE number 1614707 (Why is no real title available?) | 2001-07-05 | Paper |
| scientific article; zbMATH DE number 1538015 (Why is no real title available?) | 2000-12-03 | Paper |
| scientific article; zbMATH DE number 1405623 (Why is no real title available?) | 2000-02-23 | Paper |
| scientific article; zbMATH DE number 1348468 (Why is no real title available?) | 1999-10-10 | Paper |
Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
Theoretical Computer Science | 1999-01-12 | Paper |
Paramodulation with built-in AC-theories and symbolic constraints
Journal of Symbolic Computation | 1997-05-28 | Paper |
A total AC-compatible ordering based on RPO
Theoretical Computer Science | 1997-02-28 | Paper |
Theorem proving with ordering and equality constrained clauses
Journal of Symbolic Computation | 1995-09-04 | Paper |
