| Publication | Date of Publication | Type |
|---|
| Algebraic reasoning for (un)solvable loops (invited talk) | 2024-12-03 | Paper |
| Non-classical logics in satisfiability modulo theories | 2024-05-17 | Paper |
| SAT-Based Subsumption Resolution | 2024-04-26 | Paper |
| Program Synthesis in Saturation | 2024-04-26 | Paper |
The probabilistic termination tool amber
Formal Methods in System Design | 2024-01-08 | Paper |
| ALASCA: reasoning in quantified linear arithmetic | 2023-12-13 | Paper |
Algebra-Based Loop Analysis
Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation | 2023-11-03 | Paper |
From Polynomial Invariants to Linear Loops
Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation | 2023-11-03 | Paper |
Algebra-Based Reasoning for Loop Synthesis
Formal Aspects of Computing | 2023-08-31 | Paper |
Symbolic computation in automated program reasoning
Formal Methods | 2023-08-17 | Paper |
What else is undecidable about loops?
Relational and Algebraic Methods in Computer Science | 2023-08-17 | Paper |
Getting saturated with induction
Lecture Notes in Computer Science | 2023-08-10 | Paper |
Solving invariant generation for unsolvable loops
Static Analysis | 2023-07-28 | Paper |
Distribution estimation for probabilistic loops
Quantitative Evaluation of Systems | 2023-06-02 | Paper |
Lemmaless induction in trace logic
Lecture Notes in Computer Science | 2023-06-02 | Paper |
| Algebra-Based Loop Synthesis | 2023-03-21 | Paper |
Lonely points in simplices
Discrete & Computational Geometry | 2023-01-23 | Paper |
Subsumption demodulation in first-order theorem proving
(available as arXiv preprint) | 2022-11-09 | Paper |
| Inductive benchmarks for automated reasoning | 2022-04-22 | Paper |
| Automated generation of exam sheets for automated deduction | 2022-04-22 | Paper |
Moment-based analysis of Bayesian network properties
Theoretical Computer Science | 2022-02-01 | Paper |
| Integer induction in saturation | 2021-12-01 | Paper |
Automated termination analysis of polynomial probabilistic programs
(available as arXiv preprint) | 2021-10-18 | Paper |
Algebra-based synthesis of loops and their invariants (invited paper)
(available as arXiv preprint) | 2021-10-18 | Paper |
Analysis of Bayesian networks via prob-solvable loops
(available as arXiv preprint) | 2021-07-08 | Paper |
Induction with generalization in superposition reasoning
Lecture Notes in Computer Science | 2021-01-20 | Paper |
Formalizing graph trail properties in Isabelle/HOL
Lecture Notes in Computer Science | 2021-01-20 | Paper |
Automated generation of non-linear loop invariants utilizing hypergeometric sequences
Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation | 2020-09-09 | Paper |
Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
Invariant generation for multi-path loops with polynomial assignments
Lecture Notes in Computer Science | 2020-07-07 | Paper |
Loop Analysis by Quantification over Iterations
EPiC Series in Computing | 2019-07-04 | Paper |
First-order interpolation and interpolating proof systems
EPiC Series in Computing | 2019-01-10 | Paper |
Aligator.jl -- a Julia package for loop invariant generation
(available as arXiv preprint) | 2018-10-18 | Paper |
| A FOOLish encoding of the next state relations of imperative programs | 2018-10-18 | Paper |
Coming to terms with quantified reasoning
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Splitting proofs for interpolation
(available as arXiv preprint) | 2017-09-22 | Paper |
Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution
Journal of Symbolic Computation | 2017-02-06 | Paper |
Segment Abstraction for Worst-Case Execution Time Analysis
Programming Languages and Systems | 2016-04-26 | Paper |
Reasoning about loops using Vampire in KeY
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
Extensional crisis and proving identity
Automated Technology for Verification and Analysis | 2015-12-17 | Paper |
Symbolic Loop Bound Computation for WCET Analysis
Perspectives of Systems Informatics | 2015-12-07 | Paper |
Lingva: generating and proving program properties using symbol elimination
Lecture Notes in Computer Science | 2015-12-03 | Paper |
A First Class Boolean Sort in First-Order Theorem Proving and TPTP
Lecture Notes in Computer Science | 2015-11-20 | Paper |
Playing in the grey area of proofs
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Tree Interpolation in Vampire
Logic for Programming, Artificial Intelligence, and Reasoning | 2014-01-17 | Paper |
On transfinite Knuth-Bendix orders
Lecture Notes in Computer Science | 2011-07-29 | Paper |
ABC: algebraic bound computation for loops
Logic for Programming, Artificial Intelligence, and Reasoning | 2011-01-07 | Paper |
Aligators for Arrays (Tool Paper)
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
| Solving the four fundamental problems from the theory of profile grids via BEM | 2010-09-17 | Paper |
| Deciding properties of affine loops | 2010-09-17 | Paper |
Interpolation and symbol elimination in Vampire
Automated Reasoning | 2010-09-14 | Paper |
A complete invariant generation approach for P-solvable loops
Perspectives of Systems Informatics | 2010-02-02 | Paper |
Invariant and type inference for matrices
Lecture Notes in Computer Science | 2010-01-14 | Paper |
Interpolation and Symbol Elimination
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Valigator: A Verification Tool with Bound and Invariant Generation
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Aligator: A Mathematica Package for Invariant Generation (System Description)
Automated Reasoning | 2008-11-27 | Paper |
Invariant Generation for P-Solvable Loops with Assignments
Computer Science – Theory and Applications | 2008-06-05 | Paper |
Reasoning Algebraically About P-Solvable Loops
Tools and Algorithms for the Construction and Analysis of Systems | 2008-04-11 | Paper |
\textit{Theorema}: Towards computer-aided mathematical theory exploration
Journal of Applied Logic | 2007-02-20 | Paper |
| Automated generation of loop invariants by recurrence solving in \texttt{Theorema} | 2007-01-22 | Paper |
| scientific article; zbMATH DE number 2217740 (Why is no real title available?) | 2005-10-26 | Paper |
Linear Loop Synthesis for Quadratic Invariants
(available as arXiv preprint) | N/A | Paper |
