Erweiterte Suche


Zielgruppennavigation: 

 

Hauptnavigation: 

Sprache:

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

Dr. Peter Lammich

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

Anschrift

Raum 1.11.61
Institut für Informatik
Boltzmannstrasse 3
85748 Garching

Forschungsinteressen

(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

Isabelle/HOL Projekte

Auf eigener Seite.

Lebenslauf

  • 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

Lehre

Siehe Lehre-Seite.

Publikationen

  • 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)
Impressum | © 2007 FB10 WWU Münster
Universität Münster
Schlossplatz 2 - 48149 Münster
Tel.: +49 (251) 83-0 - Fax: +49 (251) 83-3 20 90
E-Mail: