Publications

Filter by type:

. Machine learning-based run-time anomaly detection in software systems: An industrial evaluation. Machine Learning Techniques for Software Quality Evaluation (MaLTeSQuE 2018), 2018.

PDF DOI

. Partiality and recursion in interactive theorem provers: An overview. Mathematical Structures in Computer Science 26(1): 38-88, 2016.

PDF DOI

. Scalable LCF-style proof translation. Interactive Theorem Proving (ITP 2013), 2013.

PDF DOI

. Data refinement in Isabelle/HOL. Interactive Theorem Proving (ITP 2013), 2013.

PDF DOI

. Proof Pearl: Regular expression equivalence and relation algebra. Journal of Automated Reasoning, 49(1):95–106, 2012.

PDF DOI

. Termination of Isabelle functions via termination of rewriting. Interactive Theorem Proving (ITP 2011), 2011.

PDF DOI

. Monotonicity inference for higher-order formulas. Journal of Automated Reasoning, 47(4): 369–398, 2011.

PDF DOI

. Adding soft types to Isabelle. Unpublished internal note, 2010.

PDF

. Recursive definitions of monadic functions. Partiality and Recursion in Interactive Theorem Proving (PAR 2010), 2010.

PDF DOI

. A mechanized translation from higher-order logic to set theory. Interactive Theorem Proving (ITP 2010), 2010.

PDF DOI

. Partial and nested recursive function definitions in higher-order logic. Journal of Automated Reasoning, 44(4):303–336, 2010.

PDF DOI

. Monotonicity inference for higher-order formulas. Automated Reasoning (IJCAR 2010), 2010.

PDF DOI

. Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Dissertation. Technische Universität München, 2009.

PDF Official Library Website

. A mechanized proof reconstruction for SCNP termination (extended abstract). In International Workshop on Termination (WST’09), 2009.

PDF

. Shallow dependency pairs. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, TPHOLs 2008: Emerging Trends Proceedings, 2008. Department of Electrical and Computer Engineering, Concordia University., 2008.

PDF

. Pattern minimization problems over recursive data types. International Conference on Functional Programming (ICFP 2008), 2008.

PDF DOI

. Imperative functional programming in Isabelle/HOL. Theorem Proving in Higher-Order Logics (TPHOLs 2008), 2008.

PDF DOI

. Finding lexicographic orders for termination proofs in Isabelle/HOL. Theorem Proving in Higher-Order Logics (TPHOLs 2007), 2007.

PDF DOI

. Certified size-change termination. Automated Deduction (CADE 2007), 2007.

PDF DOI

. Partial recursive functions in higher-order logic. Automated Reasoning (IJCAR 2006), 2006.

PDF DOI

. Programmverifikation mit Modulen und Axiomatischen Spezifikationen in VeriFun. Diploma Thesis, Technische Universität Darmstadt, 2005.

PDF