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

Publications

The layout of the preprint versions provided on this page may differ from the original versions.
  • Heiko Mantel, Markus Müller-Olm, Matthias Perner, Alexander Wenner.
    Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis.
    In Post-Proceedings of Logic-Based Program Synthesis and Transformation (LOPSTR). July, 2015.
    LNCS 9527. Springer International Publishing.
    lopstr2015.pdf ©Springer
    Extended Version with Appendix: lopstr2015_app.pdf

  • Benedikt Nordhoff, Markus Müller-Olm and Peter Lammich
    Iterable Forward Reachability Analysis of Monitor-DPNs
    In Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff: Proceedings Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (Festschrift for Dave Schmidt), Manhattan, Kansas, USA, 19-20th September 2013, Electronic Proceedings in Theoretical Computer Science 129, pp. 384-403. http://dx.doi.org/10.4204/EPTCS.129.24, September 2013.

  • Peter Lammich, Markus Müller-Olm, Helmut Seidl, Alexander Wenner.
    Contextual Locking for Dynamic Pushdown Networks.
    In Proceedings of SAS 2013 (20th Static Analysis Symposium), LNCS 7935. Springer, 2013.
    sas13.pdf ©Springer

  • Andrea Flexeder, Markus Müller-Olm, Michael Petter, and Helmut Seidl.
    Fast Interprocedural Linear Two Variable Equalities.
    ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), December 2011.

  • Martin Schwarz, Helmut Seidl, Vesal Vojdani, Markus Müller-Olm, and Peter Lammich.
    Static Analysis of Interrupt-Driven Programs Synchronized via the Priority Ceiling Protocol.
    In Proc. of POPL 2011 (Principles of Programming Languages), January 26-28, 2011, Austin, Texas, USA.

  • 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), LNCS 6538, pages 199-213. Springer, 2011. vmcai11.pdf ©Springer
    Extended Version with proofs: vmcai11extended.pdf

  • 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

  • Alexander Wenner.
    Weighted Dynamic Pushdown Networks.
    In Proceedings of 19th European Symposium on Programming (ESOP 2010), LNCS 6012, pages 590-609. Springer, 2010.
    esop10.pdf ©Springer

  • Peter Lammich
    Isabelle Collections Framework.
    In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, November 2009.
    Formal proof development.
    http://afp.sourceforge.net/entries/Collections.shtml
  • Peter Lammich
    Tree Automata.
    In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, November 2009.
    Formal proof development.
    http://afp.sourceforge.net/entries/Tree-Automata.shtml
  • Peter Lammich, Markus Müller-Olm, and Alexander Wenner.
    Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints.
    In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification (Proc. 21st International Concerence, CAV'09), LNCS 5643, pages 525-539. Springer, 2009.
    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

  • Neil D. Jones and Markus Müller-Olm (Eds.).
    Verification, Model Checking, and Abstract Interpretation.
    10th International Conference, VMCAI 2009, Savannah, GA, USA, January 2009, Proceedings.
    LNCS 5403. Springer, 2009.
    Available online from SpringerLink (access to full papers is restricted to LNCS subscribers) ©Springer

  • 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 and Markus Müller-Olm.
    Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors.
    In Maria Alpuente and German Vidal, editors, Static Analysis (Proc. 15th International Symposium, SAS 2008), LNCS 5079, pages 205-220. Springer, 2008.
    sas08.ps.gz or sas08.pdf ©Springer
    Technical Report version with appendices, March 2008:
    tr-conflict-analysis.ps or tr-conflict-analysis.pdf

  • Markus Müller-Olm and Helmut Seidl.
    Upper Adjoints for Fast Inter-Procedural Variable Equalities.
    In Sophia Drossopoulou, editor, Programming Languages and Systems (Proc. 17th European Symposium on Programming, ESOP 2008), LNCS 4960, pages 178-192. Springer, 2008.
    esop08.ps.gz or esop08.pdf ©Springer

  • Peter Lammich and Markus Müller-Olm.
    Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors.
    In G. Klein, T. Nipkow, and L. Paulson, editors, The Archive of Formal Proofs, December 2007.
    Formal proof development.
    http://afp.sourceforge.net/entries/Program-Conflict-Analysis.shtml

  • Markus Müller-Olm and Helmut Seidl.
    Analysis of Modular Arithmetic.
    ACM Trans. Program. Lang. Syst. (TOPLAS) 29(5), August 2007.
    toplas-preprint-modulo.ps.gz or toplas-preprint-modulo.pdf

  • Peter Lammich and Markus Müller-Olm.
    Precise Fixpoint-Based Analysis of Programs with Thread-Creation and Procedures.
    In L. Caires, V.T. Vasconcelos, editors, CONCUR 2007: Concurrency Theory, LNCS 4703, pages 287-302. Springer, 2007.
    concur07.ps.gz or concur07.pdf ©Springer
    Version with appendix: concur07-extend.ps.gz or concur07-extend.pdf

  • Markus Müller-Olm.
    Variations on Constants: Flow Analysis of Sequential and Parallel Programs.
    Monograph, LNCS 3800, Springer, 2006.

  • Markus Müller-Olm, Michael Petter, and Helmut Seidl.
    Interprocedurally Analyzing Polynomial Identities.
    In B. Durand and W. Thomas, editors, STACS 2006 (Symposium on Theoretical Aspects of Computer Science), LNCS 3884, pages 50-67. Springer, 2006.
    stacs06.ps.gz or stacs06.pdf ©Springer

  • Ahmed Bouajjani, Markus Müller-Olm, and Tayssir Touili.
    Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems.
    In Martin Abadi and Luca de Alfaro, editors, Concurrency Theory (Proc. 16th International Conference, CONCUR 2005), LNCS 3653, pages 473-487. Springer, 2005.
    concur05.ps.gz or concur05.pdf ©Springer
    Extended version with proofs: concur05-long.ps.gz or concur05-long.pdf

  • Markus Müller-Olm and Helmut Seidl.
    A Generic Framework for Interprocedural Analysis of Numerical Properties.
    In Chris Hankin and Igor Siveroni, editors, Static Analysis (Proc. 12th International Symposium, SAS 2005), LNCS 3672, pages 235-250. Springer, 2005.
    sas05.ps.gz or sas05.pdf ©Springer

  • Markus Müller-Olm, Helmut Seidl, and Bernhard Steffen.
    Interprocedural Herbrand Equalities.
    In Mooly Sagiv, editor, Programming Languages and Systems (Proc. 14th European Symposium on Programming, ESOP 2005), LNCS 3444, pages 31-45. Springer, 2005.
    esop05-herbrand.ps.gz or esop05-herbrand.pdf ©Springer

  • Markus Müller-Olm and Helmut Seidl.
    Analysis of Modular Arithmetic.
    In Mooly Sagiv, editor, Programming Languages and Systems (Proc. 14th European Symposium on Programming, ESOP 2005), LNCS 3444, pages 46-60. Springer, 2005.
    esop05-modulo.ps.gz or esop05-modulo.pdf ©Springer

  • Markus Müller-Olm, Oliver Rüthing, and Helmut Seidl.
    Checking Herbrand Equalities and Beyond.
    In Radhia Cousot, editor, VMCAI 2005 (Sixth International Conference on Verification, Model Checking, and Abstract Interpretation), LNCS 3385, pages 79-96. Springer, 2005.
    vmcai05.ps.gz or vmcai05.pdf ©Springer

  • Markus Müller-Olm, Helmut Seidl, and Bernhard Steffen.
    Interprocedural Analysis (Almost) for Free.
    Technical Report 790, Fachbereich Informatik, Universität Dortmund, July 2004.
    tr-do790.ps.gz or tr-do-790.pdf

  • Markus Müller-Olm and Helmut Seidl.
    Interprocedural Analysis of Modular Arithmetic.
    Technical Report 789, Fachbereich Informatik, Universität Dortmund, July 2004.
    tr-do789.ps.gz or tr-do789.pdf

  • Markus Müller-Olm, Oliver Rüthing, and Helmut Seidl.
    Testing Herbrand Equalities and Beyond.
    Technical Report 788, Fachbereich Informatik, Universität Dortmund, July 2004.
    tr-do788.ps.gz or tr-do788.pdf

  • Markus Müller-Olm and Helmut Seidl.
    A Note on Karr's Algorithm.
    International Colloquium on Automata, Languages, and Programming (ICALP'04), July 12-16, 2004, Turku, Finland.
    icalp04.ps.gz or icalp04.pdf ©Springer

  • Markus Müller-Olm and Haiseung Yoo.
    MetaGame: An animation tool for model-checking games.
    Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), March 29-April 2, 2004, Barcelona, Spain.
    tacas04.ps.gz or tacas04.pdf ©Springer

  • Markus Müller-Olm and Helmut Seidl.
    Computing polynomial program invariants.
    Information Processing Letters (IPL) 91(5), pages 233-244, 2004.
    (Preliminary version appeared as technical report of FernUniversität Hagen, Fachbereich Informatik, TR-310, October 2003.)
    ipl-poly-preprint.ps.gz or ipl-poly-preprint.pdf ©Elsevier

  • Markus Müller-Olm and Helmut Seidl.
    Precise interprocedural analysis through linear algebra.
    Proceedings of Principles of Programming Languages (POPL'04), January 14-16, 2004, Venice, Italy.
    popl04.ps.gz or popl04.pdf ©ACM

  • Markus Müller-Olm.
    Precise interprocedural dependence analysis of parallel programs.
    Theoretical Computer Science (TCS) 31(1), pages 325-388, 2004.
    tcsb-979.ps.gz or tcsb-979.pdf ©Elsevier

  • Helmut Seidl, Varmo Vene, and Markus Müller-Olm.
    Global invariants for analysing multi-threaded applications.
    Proc. of Estonian Academy of Sciences: Phys., Math., volume 52, nr. 4, pages 413-436, 2003.
    globInv.ps.gz or globInv.pdf ©Estonian Academy Publishers

  • Rudolf Berghammer and Markus Müller-Olm.
    Formal development and verification of approximation algorithms using auxiliary variables.
    Workshop on Logic-Based Program Development and Transformation (LOPSTR'03), August 25-27, 2003, Uppsala, Schweden. Revised version appeared in LNCS 3018, pp. 59-74. Springer 2004.
    lopstr03pre.ps.gz or lopstr03pre.pdf

  • Markus Müller-Olm and Helmut Seidl.
    Computing interprocedurally valid relations in affine programs.
    Technical Report, University of Trier, January 2003.
    Revised version appeared in POPL 2004 under modified title Precise Interprocedural Analysis through Linear Algebra.
    affineTRTrier.ps.gz or affineTRTrier.pdf

  • Markus Müller-Olm.
    Variations on Constants.
    Habilitation thesis, Fachbereich Informatik, Universität Dortmund. August 2002.
    habil.ps.gz or habil.pdf

  • Markus Müller-Olm and Helmut Seidl.
    Polynomial constants are decidable.
    In M. V. Hermenegildo and German Puebla, editors, SAS 2002 (9th Static Analysis Symposium), LNCS 2477, pages 4-19. Springer, 2002.
    sas02.ps.gz or sas02.pdf ©Springer

  • Markus Müller-Olm and Helmut Seidl.
    On optimal slicing of parallel programs.
    In STOC 2001 (33th ACM Symposium on Theory of Computing), pages 647-656. © ACM Press, 2001.
    stoc01.ps.gz or stoc01.pdf ©ACM

  • Markus Müller-Olm and Oliver Rüthing.
    The complexity of constant propagation.
    In D. Sands, editor, ESOP 2001 (10th European Symposium on Programming), LNCS 2028, pages 190-205. Springer, 2001.
    esop01.ps.gz or esop01.pdf ©Springer

  • Markus Müller-Olm.
    The complexity of copy constant detection in parallel programs.
    In Afonso Ferreira and Horst Reichel, editors, STACS 2001 (Symposium on Theoretical Aspects of Computer Science), LNCS 2010, pages 490-501. Springer, 2001.
    stacs01.ps.gz or stacs01.pdf ©Springer

  • Markus Müller-Olm and Andreas Wolf.
    On the translation of procedures to finite machines: Abstraction allows a clean proof.
    In Gert Smolka, editor, Programming Languages and Systems: ESOP'2000, LNCS 1782, pages 290-304. Springer, 2000.
    esop00.ps.gz or esop00.pdf ©Springer

  • Martin Fränzle and Markus Müller-Olm.
    Compilation and synthesis for real-time embedded controllers.
    In B. Steffen and E.-R. Olderog, editors, Correct System Design: Recent Insights and Advances, LNCS 1710, pages 256-287. Springer, 1999.
    hl-band.ps.gz or hl-band.pdf ©Springer

  • Markus Müller-Olm and Andreas Wolf.
    On excusable and inexcusable failures: Towards an adequate notion of translation correctness.
    In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99: Formal Methods, LNCS 1709, pages 1107-1127. Springer, 1999.
    fm99.ps.gz or fm99.pdf ©Springer

  • Martin Fränzle, Wolfgang Goerigk, Burghard von Karger, and Markus Müller-Olm.
    Beyond ProCoS at Kiel: A synopsis of recent research.
    ProCoS WG workshop at FM'99, available from FM'99 CD-Rom, Springer, September 1999.
    fm99procos.ps.gz or fm99procos.pdf

  • Markus Müller-Olm, David Schmidt, and Bernhard Steffen.
    Model-checking: A tutorial introduction.
    In A. Cortesi and G. Filé, editors, Static Analysis: SAS'99, LNCS 1694, pages 330-354. Springer, 1999.
    sas99.ps.gz or sas99.pdf ©Springer

  • Markus Müller-Olm, Bernhard Steffen, and Rance Cleaveland.
    On the evolution of reactive components: A process-algebraic approach.
    In Jean-Pierre Finance, editor, FASE'99, LNCS 1577, pages 161-175. Springer, 1999.
    fase99.ps.gz or fase99.pdf ©Springer

  • Markus Müller-Olm.
    A modal fixpoint logic with chop.
    In Christoph Meinel and Sophie Tison, editors, STACS'99, LNCS 1563, pages 510-520. Springer, 1999.
    stacs99.ps.gz or stacs99.pdf

  • Markus Müller-Olm.
    Derivation of characteristic formulae.
    Electronic Notes in Theoretical Computer Science, 18:12, August 1998.
    http://www.elsevier.nl/locate/entcs/volume18.html.
    mfcs98.ps.gz or mfcs98.pdf

  • Markus Müller-Olm.
    Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction.
    Monograph, LNCS 1283, Springer, 1997.
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: