Office: S2|02 E319 Phone: +49 6151 16-50173 Fax: +49 6151 16-5326 Mail: aderholdmais.informatik.tu-darmstadt.de Office Hour: Tuesday, 13:15–14:15

TU Darmstadt Department of Computer Science Modeling and Analysis of Information Systems Hochschulstraße 10 D-64289 Darmstadt Germany

Research Interests

• formal methods for software security
• best practices for software development
• information flow security
  
• automated reasoning and theorem proving

Services to the Scientific Community

• Organizer of the RS3 Tutorial on Information Flow Security and Verification Tools, Buchenau, Germany, 10–13 October 2011
• Co-Chair and Co-Organizer of Verify-2010: 6th International Verification Workshop, affiliated with FLoC/IJCAR, Edinburgh, UK, 20–21 July 2010
• PC Member of Calculemus 2010: 17th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Paris, France, 5–10 July 2010
• PC Member of Calculemus 2009: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Ontario, Canada, 6–7 July 2009
• Organizer of the 17th CIAO Workshop 2008, Darmstadt, Germany, 20–22 February 2008

Teaching

• Integrated Course: Static and Dynamic Program Analysis (6 CP, lectures and tutorials, together with Prof. Heiko Mantel, winter 2012/2013)
• Lab Course: Secure Coding Lab (6 CP, summer 2012)
• Integrated Course: Static and Dynamic Program Analysis (6 CP, lectures and tutorials, together with Prof. Heiko Mantel, winter 2011/2012)

Publications

• Markus Aderhold, Serge Autexier, and Heiko Mantel. Proceedings of the 6th International Verification Workshop (VERIFY-2010). Workshop in connection with the Federated Logic Conference (FLoC-2010). EPiC Series, vol. 3, 2012.
• Markus Aderhold. Second-Order Programs with Preconditions. In Simon Siegler and Nathan Wasser, editors, Verification, Induction, Termination Analysis: Festschrift for Christoph Walther on the Occasion of His 60th Birthday, Lecture Notes in Artificial Intelligence, vol. 6463, pp. 129–143, Springer-Verlag, 2010. [PDF] [BibTeX]
• Markus Aderhold. Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion. In Jürgen Giesl and Reiner Hähnle, editors, Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR-5), Lecture Notes in Artificial Intelligence, vol. 6173, pp. 263–277, Springer-Verlag, 2010. [PDF] [BibTeX]
• Markus Aderhold, Jorge Cuéllar, Heiko Mantel, and Henning Sudbrock. Exemplary Formalization of Secure Coding Guidelines. Technical Report TUD-CS-2010-0060, TU Darmstadt, 2010.
• Markus Aderhold. Automated Termination Analysis for Programs with Second-Order Recursion. In Javier Esparza and Rupak Majumdar, editors, Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS-16), Lecture Notes in Computer Science, vol. 6015, pp. 221–235, Springer-Verlag, 2010. [PDF] [BibTeX]
  
• Markus Aderhold. Verification of Second-Order Functional Programs. Doctoral dissertation, Technische Universität Darmstadt, Germany, 2009. [BibTeX]
• Markus Aderhold. Proving Termination of Programs with Second-Order Recursion. Extended abstract in Proceedings of the 10th International Workshop on Termination (WST-10), pp. 4–7, 2009.
• Markus Aderhold. Automated Termination Analysis for Programs with Second-Order Recursion. Technical Report, FG Programmiermethodik, Technische Universität Darmstadt, 2009.
• Markus Aderhold. Improvements in Formula Generalization. In Frank Pfenning, editor, Proceedings of the 21st Conference on Automated Deduction (CADE-21), Lecture Notes in Artificial Intelligence, vol. 4603, pp. 231–246, Springer-Verlag, 2007. [PDF] [BibTeX]
• Andreas Schlosser, Christoph Walther, Michael Gonder, and Markus Aderhold. Context Dependent Procedures and Computed Types in VeriFun. In Aaron Stump, Hongwei Xi, editors, Proceedings of the 1st Workshop Programming Languages meet Program Verification, Electronic Notes in Theoretical Computer Science, 174(7):61–78, 2007.
• Markus Aderhold, Christoph Walther, Daniel Szallies, and Andreas Schlosser. A Fast Disprover for VeriFun. In Wolfgang Ahrendt, Peter Baumgartner, and Hans de Nivelle, editors, Proceedings of the Third Workshop on Disproving, pp. 59–69, IJCAR 2006, Seattle (WA), USA, 2006. [BibTeX]
• Andreas Schlosser, Christoph Walther, and Markus Aderhold. Axiomatic Specifications in VeriFun. In Serge Autexier and Heiko Mantel, editors, Proceedings of the 3rd Verification Workshop, pp. 146–163, IJCAR 2006, Seattle (WA), USA, 2006.
• Christoph Walther, Markus Aderhold, and Andreas Schlosser. The L 1.0 Primer. Technical Report VFR 06/01, FG Programmiermethodik, Technische Universität Darmstadt, 2006.
• Markus Aderhold. Formula Generalization in VeriFun. Diploma thesis, FG Programmiermethodik, Technische Universität Darmstadt, Germany, 2004. [BibTeX]
• Markus Aderhold and James Slack. Embedding Balanced Binary Trees in the Hypercube. Department of Computer Science, University of British Columbia, Canada, 2003.
• Markus Aderhold. Embedding Strongly Balanced Binary Trees in the Hypercube. Department of Computer Science, University of British Columbia, Canada, 2002.