Prof. Dr. Markus Müller-Olm

Kontakt

Portrait
Professur für Praktische Informatik (Prof. Müller-Olm)
Einsteinstraße 62
Raum 716
48149 Münster

Forschungsschwerpunkte

  • Programmanalyse
  • Softwareverifikation
  • Theorie der Parallelität

Vita

Akademische Ausbildung

2003Habilitation, Fachbereich Informatik, Universität Dortmund, Venia Legendi für Informatik, Titel der Habilitationsschrift: Variations on Constants - Flow Analysis of Sequential and Parallel Programs
1996Promotion zum Dr. rer. nat. (summa cum laude), Technische Fakultät, Christian-Albrechts-Universität, Kiel, Dissertationsthema: Modular Compiler Verification, Betreuer: Prof. Hans Langmaack
1991Diplom in Informatik, Christian-Albrechts-Universität, Kiel

Beruflicher Werdegang

seit 10/2005Universitätsprofessor, Institut für Informatik, FB 10, WWU Münster, Leiter der Arbeitsgruppe Softwareentwicklung und Verifikation
10/2004 - 09/2005Hochschuldozent, Fachbereich Informatik, Universität Dortmund
04/2003 - 09/2004Lehrstuhlvertretung, Lehrgebiet Programmiersprachen und Softwarekonstruktion, Fachbereich Informatik, FernUniversität Hagen
01/1997 - 03/2003Wissenschaftlicher Mitarbeiter, Universitäten Passau, Dortmund und Trier
04/1991 - 12/1996Wissenschaftlicher Mitarbeiter, Institut für Informatik und Angewandte Mathematik, CAU Kiel

Mitgliedschaften und Aktivitäten in Gremien

seit 2003Mitglied und Secretary (seit Herbst 2012) der IFIP Working Group 2.2, Formal Description of Programming Concepts
seit 2002Mitglied von Programmkommitees internationaler Konferenzen, Workshops und Doktorandenschulen, u.a. ESOP'19, SETTA'18, NETYS'18, SETTA'17, SETTA'16, ICALP'15, SAS'14, RP'13, ACM SAC'13, SAS'12, FOSSACS'12, ACM SAC'12, MOVEP'12, CONCUR'10, CAV'10, FOSSACS'10, MOVEP'10, VMCAI'10, ICALP'09, CAV'09, VMCAI'09, MOVEP'08, VMCAI'07, VMCAI'06, MOVEP'06, ESOP'04, MOVEP'04, VMCAI'04, COCV'02
2017 - 2018Programmkomitee-Chair (mit Xinyu Feng, Nanjing University, China, und Zijiang Yang, Western Michigan University, USA) von SETTA 2018: 4th Symposium on Dependable Software Engineering, Beijing, China, 4.-6. September 2018
2013 - 2017Stellvertretender Sprecher der GI-Fachgruppe Concurrency Theory
2013 - 2014Programmkomitee-Chair (mit Helmut Seidl) von SAS'14: 21th International Static Analysis Symposium, München, Germany, 13.-15. September 2014
2008 - 2009Programmkomitee-Chair (mit Neil D. Jones) von VMCAI'09: 10th International Conference on Verification, Model Checking and Abstract Interpretation, Savannah, GA, USA, January 18-20, 2009

Publikationen

  • Mantel Heiko, Müller-Olm Markus, Perner Matthias, Wenner Alexander. 2015. ‘Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis.’ In Logic-Based Program Synthesis and Transformation, edited by Falaschi Moreno.: Springer International Publishing. doi: 10.1007/978-3-319-27436-2_12.
  • Nordhoff Benedikt, Müller-Olm Markus, Lammich Peter. 2013. ‘Iterable Forward Reachability Analysis of Monitor-DPNs.’ In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, edited by Banerjee A, Danvy O, Doh K, Hatcliff J, 384-403. Manhattan, Kansas, USA: Open Publishing Association. doi: 10.4204/EPTCS.129.24.
  • Lammich Peter, Müller-Olm Markus, Seidl Helmut, Wenner Alexander. 2013. ‘Contextual Locking for Dynamic Pushdown Networks.’ In 20th Static Analysis Symposium, edited by Francesco Logozzo, Manuel Fahndrich, 477-498.: Springer.
  • Flexeder Andrea, Müller-Olm Markus, Petter Michael, Seidl Helmut. 2011. ‘Fast interprocedural linear two variable equalities.’ ACM Transactions on Programming Languages and Systems 33, Nr. 6.
  • Jones Neil D., Müller-Olm Markus. 2011. ‘Preface to a special section on verification, model checking, and abstract interpretation.’ International Journal on Software Tools for Technology Transfer 13, Nr. 6: 491-493. doi: 10.1007/s10009-011-0214-x.
  • Gawlitza Thomas, Lammich Peter, Müller-Olm Markus, Seidl Helmut, Wenner Alexander. 2011. ‘Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation.’ In Verification, Model Checking and Abstract Interpretation, edited by Jhala Ranjit, Schmidt David, 199-213. Berlin, Heidelberg, New York: Springer-Verlag. doi: 10.1007/978-3-642-18275-4_15.
  • Kuchen H, Majchrzak TA, Müller-Olm M, Ed. 2011. Tagungsband 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'11). Münster: Institut für Wirtschaftsinformatik, WWU Münster.
  • Schwarz Martin D., Seidl Helmut, Vojdani Vesal, Lammich Peter, Müller-Olm Markus. 2011. ‘Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol.’ In Conference Record of the 38th Annual ACM Symposium on Principles of Programming Languages, edited by Ball Thomas, Sagiv Mooly, 93-104.: ACM. doi: 10.1145/1926385.1926398.
  • Lammich Peter, Müller-Olm Markus, Wenner Alexander. 2009. ‘Predecessor sets of dynamic pushdown networks with tree-regular constraints.’ In Computer Aided Verification, edited by Bouajjani Ahmed, Maler Oded, 525-539.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-642-02658-4_39.
  • Jones Neil D., Müller-Olm Markus, Ed. 2009. Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg, New York: Springer-Verlag. doi: 10.1007/978-3-540-93900-9.
  • Lammich Peter, Müller-Olm Markus. 2008. ‘Conflict analysis of programs with procedures, dynamic thread creation, and monitors.’ In Static analysis, edited by Alpuente María, Vidal Germán, 205-220. Berlin: Springer. doi: 10.1007/978-3-540-69166-2_14.
  • Müller-Olm Markus, Seidl Helmut. 2008. ‘Upper adjoints for fast inter-procedural variable equalities.’ In Programming Languages and Systems, edited by Drossopoulou Sophia, 178-192.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-78739-6_15.
  • Müller-Olm Markus, Seidl Helmut. 2007. ‘Analysis of modular arithmetic.’ ACM Transactions on Programming Languages and Systems 29, Nr. 5. doi: 10.1145/1275497.1275504.
  • Lammich Peter, Müller-Olm Markus. 2007. ‘Precise fixpoint-based analysis of programs with thread-creation and procedures.’ In CONCUR 2007 - Concurrency Theory, edited by Caires Luís, Vasconcelos Vasco T., 287-302. Berlin: Springer. doi: 10.1007/978-3-540-74407-8_20.
  • Müller-Olm Markus. 2006. Variations on Constants: Flow Analysis of Sequential and Parallel Programs. Berlin, Heidelberg, New York: Springer-Verlag. doi: 10.1007/11871743.
  • Müller-Olm Markus, Petter Michael, Seidl Helmut. 2006. ‘Interprocedurally analyzing polynomial identities.’ In STACS 2006, edited by Durand Bruno, Thomas Wolfgang, 50-67. Berlin: Springer. doi: 10.1007/11672142_3.
  • Bouajjani Ahmed, Müller-Olm Markus, Touili Tayssir. 2005. ‘Regular symbolic analysis of dynamic networks of pushdown systems.’ In CONCUR 2005 - Concurrency Theory, edited by Abadi Martín, de Alfaro Luca, 473-487. Berlin: Springer. doi: 10.1007/11539452_36.
  • Müller-Olm Markus, Seidl Helmut. 2005. ‘Analysis of modular arithmetic.’ In Programming Languages and Systems, edited by Sagiv Mooly, 46-60.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-31987-0_5.
  • Müller-Olm Markus, Rüthing Oliver, Seidl Helmut. 2005. ‘Checking Herbrand equalities and beyond.’ In Verification, Model Checking, and Abstract Interpretation, edited by Cousot Radhia, 79-96. Berlin: Springer. doi: 10.1007/978-3-540-30579-8_6.
  • Müller-Olm Markus, Seidl Helmut, Steffen Bernhard. 2005. ‘Interprocedural Herbrand equalities.’ In Programming Languages and Systems, edited by Sagiv Mooly, 31-45.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-31987-0_4.
  • Müller-Olm Markus, Seidl Helmut. 2005. ‘A generic framework for interprocedural analysis of numerical properties.’ In Static Analysis, edited by Hankin Chris, Siveroni Igor, 235-250. Berlin: Springer. doi: 10.1007/11547662_17.
  • Müller-Olm Markus, Seidl Helmut. 2004. ‘Precise interprocedural analysis through linear algebra.’ In Conference Record of the 31st Annual ACM Symposium on Principles of Programming Languages, edited by Jones Neil D., Leroy Xavier, 330-341.: ACM.
  • Müller-Olm Markus, Seidl Helmut. 2004. ‘Computing polynomial program invariants.’ Information Processing Letters 91, Nr. 5: 233-244. doi: 10.1016/j.ipl.2004.05.004.
  • Müller-Olm Markus, Seidl Helmut. 2004. ‘A note on Karr's algorithm.’ In Automata, Languages and Programming, edited by Díaz Josep, Karhumäki Juhani, Lepistö Arto, Sannella Donald, 1016-1028. Berlin: Springer. doi: 10.1007/978-3-540-27836-8_85.
  • Berghammer Rudolf, Müller-Olm Markus. 2004. ‘Formal development and verification of approximation algorithms using auxiliary variables.’ In Logic based program synthesis and transformation: Revised Selected Papers, edited by Bruynooghe, Maurice, 59-74. Berlin: Springer. doi: 10.1007/978-3-540-25938-1_6.
  • Müller-Olm Markus. 2004. ‘Precise interprocedural dependence analysis of parallel programs.’ Theoretical Computer Science 311, Nr. 1-3: 325-388. doi: 10.1016/j.tcs.2003.09.002.
  • Müller-Olm Markus, Yoo Haiseung. 2004. ‘MetaGame: An animation tool for model-checking games.’ In Tools and Algorithms for the Construction and Analysis of Systems, edited by Jensen Kurt, Podelski Andreas, 163-167.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-24730-2_14.
  • Seidl Helmut, Vene Varmo, Müller-Olm Markus. 2003. ‘Global invariants for analysing multi-threaded applications.’ Proc. Estonian Acad. Sci. Phys. Math. 52, Nr. 4: 413-436.
  • Müller-Olm Markus, Seidl Helmut. 2002. ‘Polynomial constants are decidable.’ In Static Analysis, edited by Hermenegildo Manuel V., Puebla Germán, 4-19. Berlin: Springer. doi: 10.1007/3-540-45789-5_4.
  • Müller-Olm Markus. 2001. ‘The complexity of copy constant detection in parallel programs.’ In STACS 2001, edited by Ferreira Afonso, Reichel Horst, 490-501.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-44693-1_43.
  • Müller-Olm Markus, Seidl Helmut. 2001. ‘On optimal slicing of parallel programs.’ In Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, July 6-8, 2001, Heraklion, Crete, Greece, edited by Vitter Jeffrey Scott, Spirakis Paul G., Yannakakis Mihalis, 647-656. New York: ACM. doi: 10.1145/380752.380864.
  • Müller-Olm Markus, Rüthing Oliver. 2001. ‘On the complexity of constant propagation.’ In Programming Languages and Systems, edited by Sands David, 190-205.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-45309-1_13.
  • Müller-Olm Markus, Wolf Andreas. 2000. ‘On the translation of procedures to finite machines.’ In Programming Languages and Systems, edited by Smolka Gert, 290-304.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-46425-5_19.
  • Müller-Olm Markus, Steffen Bernhard, Cleaveland Ramce. 1999. ‘On the evolution of reactive components.’ In Fundamental Approaches to Software Engineering, edited by Finance Jean-Pierre, 161-175.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-49020-3_11.
  • Müller-Olm Markus. 1999. ‘A modal fixpoint logic with chop.’ In STACS 99, edited by Meinel Christoph, Tison Sophie, 510-520. Berlin: Springer. doi: 10.1007/3-540-49116-3_48.
  • Fränzle Martin, Goerigk Wolfgang, von Karger Burghard, Müller-Olm Markus. 1999. ‘Beyond ProCoS at Kiel: A synopsis of recent research.’Contributed to the ProCoS WG workshop at FM'99, Toulouse, France.
  • Fränzle Martin, Müller-Olm Markus. 1999. ‘Compilation and synthesis for real-time embedded controllers.’ In Correct System Design, edited by Olderog Ernst-Rüdiger, Steffen Bernhard, 256-287.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-48092-7_12.
  • Müller-Olm Markus, Schmidt David, Steffen Bernhard. 1999. ‘Model-checking: A tutorial introduction.’ In Static Analysis, edited by Cortesi Agostino, Filé Gilberto, 330-354.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-48294-6_22.
  • Müller-Olm Markus, Wolf Andreas. 1999. ‘On excusable and inexcusable failures: Towards an adequate notion of translation correctness.’ In FM’99 — Formal Methods, edited by Wing Jeanette M., Woodcock Jim, Davies Jim, 1107-1127.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-48118-4_9.
  • Müller-Olm Markus. 1998. ‘Derivation of characteristic formulae.’ In Proc. MFCS'98 Workshop on Concurrency, edited by Jancar Petr, Kretinsky Mojmir, 159-170. Amsterdam: Elsevier. doi: 10.1016/S1571-0661(05)80257-9.
  • Müller-Olm Markus. 1997. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction. Berlin, Heidelberg, New York: Springer-Verlag. doi: 10.1007/BFb0027453.
  • He J., Hoare C.A.R., Fränzle M., Müller-Olm M., Olderog E.-R., Schenke M., Hansen M., Ravn A., Rischel H. 1994. ‘Provably correct systems.’ In Formal Techniques in Real-Time and Fault-Tolerant Systems, edited by Langmaack H., de Roever W.-P., Vytopil J., 288-335.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-58468-4_171.
  • Fränzle Martin, Müller-Olm Markus. 1994. ‘Towards provably correct code generation for a hard real-time programming language.’ In Compiler Construction, edited by Fritzson Peter A., 294-308.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-57877-3_20.
  • Buth Bettina, Buth Karl-Heinz, Fränzle Martin, von Karger Burghard, Lakhneche Yassine, Langmaack Hans, Müller-Olm Markus. 1992. ‘Provably correct compiler development and implementation.’ In Compiler Construction, edited by Kastens Uwe, Pfahler Peter, 141-155.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-55984-1_14.

Dissertationen

Meuth, PatrickThalamische Neurone in silico2011
Lammich, PeterLocksensitive Analyse paralleler Programme2011


Impressum | Datenschutzhinweis | © 2018 Institut
Institut
Beispielstr. 1
· 48155 Münster
Tel: +49 251 83-22223 · Fax: 0251 - 83 22 22 4
E-Mail: