Context Dependent Procedures and Computed Types in -eriFun. - Andreas Schlosser; Christoph Walther; Michael Gonder; Markus Aderhold (PLPV@IJCAR, 2006)

Improvements in Formula Generalization. - Markus Aderhold (CADE, 2007)

Verification of second-order functional programs. - Markus Axel Aderhold (2009)

Second-Order Programs with Preconditions. - Markus Aderhold (Verification, Induction, Termination Analysis, 2010)

Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion. - Markus Aderhold (IJCAR, 2010)

Automated Termination Analysis for Programs with Second-Order Recursion. - Markus Aderhold (TACAS, 2010)