Current Projects

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

Completed Projects

Logic-Based Analysis of Computation

Derivational Complexity Analysis

Termination Tools: Verification and Optimization