Navigation:

Hilfsnavigation:

Arbeitsgruppe Softwareentwicklung und Verifikation

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

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

Raum 715
Institut für Informatik
Einsteinstrasse 62
48149 Münster

(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 (mit Auszeichnung)
Seit Juni 2006: Mitarbeiter der Arbeitsgruppe Softwareentwicklung am Institut für Informatik der WWU Münster

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)