Navigation:

Hilfsnavigation:

Arbeitsgruppe Softwareentwicklung und Verifikation

Prof. Dr. Markus Müller-Olm
Institut für Informatik
Einsteinstraße 62
48149 Münster
Germany

Tel.: +49-251-83-33792
Fax: +49-251-83-33755

Ich bin seit September 2011 an der TU-München.

Raum 1.11.61
Institut für Informatik
Boltzmannstrasse 3
85748 Garching

(Siehe auch Publikationen)

Automatische, pr�zise Analyse von Modellen f�r Nebenl�ufige Programme
Anwendung von Theorembeweisern, insbesondere zur Verifikation von Programmanalyse- und Verifikationsalgorithmen.
Insbesondere kommt dabei das System Isabelle/HOL zum Einsatz. Siehe auch Isabelle Projekte

8. Dezember 1980: Geboren in Freiburg im Breisgau
Juni 2000: Abitur am Gymnasium Broich in Mülheim/Ruhr
Mai 2006: Diplom in Informatik an der Universität Dortmund
Seit Juni 2006: Mitarbeiter der Arbeitsgruppe Softwareentwicklung am Institut für Informatik der WWU Münster
Juni 2011: Promotion zum Doktor der Naturwissenschaften an der WWU Münster

Benedikt Nordhoff, Stefan Körner and Peter Lammich
Finger Trees.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Finger-Trees.shtml, October 2010, Formal proof development.
Rene Meis, Finn Nielsen and Peter Lammich
Binomial Heaps and Skew Binomial Heaps.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Binomial-Heaps.shtml, October 2010, Formal proof development.
Martin Schwarz, Helmut Seidl, Vesal Vojdani, Markus Müller-Olm, and Peter Lammich.
Static Analysis of Interrupt-Driven Programs.
In Proc. of POPL 2011 (Principles of Programming Languages), ACM Press, 2011.

Thomas Martin Gawlitza, Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner.
Join-Lock-Sensitive Forward Reachability Analysis of Concurrent Programs with Dynamic Process Creation.
In Proc. of VMCAI 2011 (Verification, Model Checking, and Abstract Interpretation), Springer, 2011.

Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas Reps.
A decision procedure for detecting atomicity violations for communicating processes with locks.
In International Journal on Software Tools for Technology Transfer (STTT), Volume 13, Number 1, 37-60
STTT10_atomicity.pdf ©Springer

Peter Lammich and Andreas Lochbihler.
The Isabelle Collections Framework.
In Proceedings of ITP 2010
LNCS 6172, pages 339-354. Springer, 2010. itp10.pdf ©Springer

Peter Lammich
Isabelle Collections Framework.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Collections.shtml, November 2009, Formal proof development.
Peter Lammich
Tree Automata.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Tree-Automata.shtml, November 2009, Formal proof development.
Peter Lammich
Tree Automata for Analyzing Dynamic Pushdown Networks.
Tagungsband des 15. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS 2009).
kps09.pdf

Peter Lammich, Markus Müller-Olm, and Alexander Wenner.
Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.
In proceedings of CAV'09,
cav09.ps.gz or cav09.pdf ©Springer
Most of the results in this paper have been verified with the theorem prover Isabelle/HOL. For details see the technical report.

Nicholas Kidd, Peter Lammich, Tayssir Touili, and Thomas Reps
A decision procedure for detecting atomicity violations for communicating processes with locks.
In Proceedings of SPIN Workshop, 2009
spin09.atomicity.pdf ©Springer
Extended version with proofs: tr-atomicity.pdf

Peter Lammich
Isabelle Formalization of Hedge-Constrained pre* and DPNs with Locks.
Technical Report, Univ. of Münster, January 2009.
Contains proofs for most of the results of our CAV'09 paper.
Proof Document Proof Outline (Proofs skipped) Sources

Peter Lammich, Markus Müller-Olm
Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.
In Proc. of SAS 2008
Conference version: [pdf] [ps] (©Springer)
Extended version: [pdf] [ps]
Peter Lammich, Markus Müller-Olm
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors.
In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, http://afp.sourceforge.net/entries/Program-Conflict-Analysis.shtml, December 2007, Formal proof development.
Peter Lammich, Markus Müller-Olm
Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.
In Proc of CONCUR 2007: 287-302:
Conference version: [pdf] [ps] (©Springer)
Version with appendix: [pdf] [ps]
Peter Lammich, Markus-Müller Olm
Precise Fixed Point Based Analysis of Programs with Thread-Creation.
In Proc. of MEMICS 2006, published by Faculty of Information Technology, Brno University of Technology, 2006. [pdf] [ps]
Peter Lammich
Fixpunktbasierte, optimale Analyse von Programmen mit Thread-Erzeugung
2006 (Diplomarbeit am Fachbereich Informatik der Universität Dortmund)