Current Projects

ARI: Automation of Rewriting Infrastructure

Completed Projects

Instantiation- and Learning-Based Methods in Equational Reasoning

Strong Modular Proof Assistance: Reasoning Across Theories

FORTissimo: Automating the First-Order Theory of Rewriting

The Fine Structure of Formal Proof Systems and their Computational Interpretations

Complexity Analysis-based Guaranteed Execution

Certification Redux

From Confluence to Unique Normal Forms: Certification and Complexity

Certifying Termination and Complexity Proofs of Programs

Complexity Analysis of Higher-Order Rewrite Systems

Interactive Proof: Proof Translation, Premise Selection, Rewriting

Automated Complexity Analysis via Transformations

Constrained Rewriting and SMT: Emerging Trends in Rewriting

Formalizing Open Induction, The Tree Theorem, and Simple Termination

Solving Non-Linear Arithmetic

Structural and Computational Proof Theory

Improving Certifiers for Termination Proofs

Confluence: Automation, Certification, Extensions

Termination Tools in Automated Reasoning

Logic-Based Analysis of Computation

Derivational Complexity Analysis

Termination Tools: Verification and Optimization