TTT2
I am one of the main developers of the Tyrolean Termination Tool 2 (TTT2),
a termination prover for term rewrite systems.
Visit the tool on its own
site.
CSI
I am one of the main developers of the confluence prover CSI.
Visit the tool on its own
site.
CaT
I am one of the main developers of the complexity prover CaT.
Visit the tool on its own
site.
MiniSmt
I am the main developer of MiniSmt, an SMT solver for non-linear (ir)rational
arithmetic.
Visit the tool on its own
site.
IsaFor/CeTA
I formalized looping nontermination and decreasing diagrams in IsaFoR,
a formalization of rewriting in the theorem prover Isabelle/HOL.
Visit IsaFoR/CeTA on its own
site.
KBCV
I have conceived the Knuth-Bendix Completion Visualizer, an interactive tool
for Knuth-Bendix completion.
Visit KBCV on its own
site.