Prof. Dr. Markus Müller-Olm

Professur für Praktische Informatik (Prof. Müller-Olm)
Prof. Dr. Markus Müller-Olm

Einsteinstr. 62, Raum 716
48149 Münster

T: +49-251-83-33765

  • Forschungsschwerpunkte

    • Programmanalyse
    • Softwareverifikation
    • Theorie der Parallelität

  • Vita

    Akademische Ausbildung

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

    Beruflicher Werdegang

    Universitätsprofessor, Institut für Informatik, FB 10, WWU Münster, Leiter der Arbeitsgruppe Softwareentwicklung und Verifikation
    Hochschuldozent, Fachbereich Informatik, Universität Dortmund
    Lehrstuhlvertretung, Lehrgebiet Programmiersprachen und Softwarekonstruktion, Fachbereich Informatik, FernUniversität Hagen
    Wissenschaftlicher Mitarbeiter, Universitäten Passau, Dortmund und Trier
    Wissenschaftlicher Mitarbeiter, Institut für Informatik und Angewandte Mathematik, CAU Kiel

    Mitgliedschaften und Aktivitäten in Gremien

    Programmkomitee-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
    Stellvertretender Sprecher der GI-Fachgruppe Concurrency Theory
    Programmkomitee-Chair (mit Helmut Seidl) von SAS'14: 21th International Static Analysis Symposium, München, Germany, 13.-15. September 2014
    Programmkomitee-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
    Mitglied und Secretary (seit Herbst 2012) der IFIP Working Group 2.2, Formal Description of Programming Concepts
    Mitglied 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

  • Publikationen

    • , , und . . „Automata and Fixpoints for Asynchronous Hyperproperties.“ Proc. ACM Program. Lang. (POPL), Nr. 5 (POPL): 1–29. doi: 10.1145/3434319.
    • , , und . . „Temporal Logics with Language Parameters.“ In Language and Automata Theory and Applications - 15th International Conference, LATA 2021, Milan, Italy, March 1-5, 2021, Proceedings, Bd. 12638 aus Lecture Notes in Computer Science, herausgegeben von Leporati Alberto, Martı́n-Vide Carlos und Shapira Claudio. Heidelberg: Springer. doi: 10.1007/978-3-030-68195-1\_14.
    • , , und . . „Propositional Dynamic Logic for Hyperproperties.“ In 31st International Conference on Concurrency Theory, Bd. 171 aus LIPIcs, herausgegeben von Kovács Laura Konnov Igor. Wadern: Dagstuhl Publishing. doi: 10.4230/LIPIcs.CONCUR.2020.50.
    • Xinyu, Feng, Markus, Müller-Olm, und Zijiang, Yang, Hrsg. . Lecture Notes in Computer Science, Bd. 10998, Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Beijing, China, Düsseldorf: Springer VDI Verlag. doi: 10.1007/978-3-319-99933-3.
    • , , und . . „A Branching Time Variant of CaRet.“ In Model Checking Software - 25th International Symposium, SPIN 2018, Bd. 10869 aus Lecture Notes in Computer Science, herausgegeben von Merino Pedro Gallardo María-del-Mar. Heidelberg: Springer. doi: 10.1007/978-3-319-94111-0\_9.
    • , und . . „Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis.“ In Logic-Based Program Synthesis and Transformation, Bd. 9527 aus Theoretical Computer Science and General Issues, herausgegeben von Falaschi Moreno. Basel: Springer International Publishing. doi: 10.1007/978-3-319-27436-2_12.
    • Müller-Olm, Markus, und Seidl, Helmut, Hrsg. . Lecture Notes in Computer Science, Bd. 8723, Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, Düsseldorf: Springer VDI Verlag. doi: 10.1007/978-3-319-10936-7.
    • , , und . . „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, Bd. 129 aus Electronic Proceedings in Theoretical Computer Science, herausgegeben von A Banerjee, O Danvy, K Doh und J Hatcliff. N/A: Selbstverlag / Eigenverlag. doi: 10.4204/EPTCS.129.24.
    • , und . . „Contextual Locking for Dynamic Pushdown Networks.“ In 20th Static Analysis Symposium, Bd. 7935 aus Lecture Notes in Computer Science, herausgegeben von Manuel Fahndrich Francesco Logozzo. Heidelberg: Springer.
    • , und . . „Fast interprocedural linear two variable equalities.“ ACM Transactions on Programming Languages and Systems, Nr. 33 (6)
    • , und . . „Preface to a special section on verification, model checking, and abstract interpretation.“ International Journal on Software Tools for Technology Transfer, Nr. 13 (6): 491–493. doi: 10.1007/s10009-011-0214-x.
    • Kuchen, H, Majchrzak, TA, und Müller-Olm, M, Hrsg. . Arbeitsberichte des Instituts für Wirtschaftsinformatik, Bd. 132, Tagungsband 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'11), Münster: Institut für Wirtschaftsinformatik.
    • , , , , und . . „Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation.“ In Verification, Model Checking and Abstract Interpretation, Bd. 6538 aus Lecture Notes in Computer Science, herausgegeben von Schmidt David Jhala Ranjit. Heidelberg: Springer. doi: 10.1007/978-3-642-18275-4_15.
    • , , , , und . . „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, herausgegeben von Sagiv Mooly Ball Thomas. New York, NY: ACM Press. doi: 10.1145/1926385.1926398.
    • , , und . . „Predecessor sets of dynamic pushdown networks with tree-regular constraints.“ In Computer Aided Verification, Bd. 5643 aus Lecture Notes in Computer Science, herausgegeben von Maler Oded Bouajjani Ahmed. Heidelberg: Springer. doi: 10.1007/978-3-642-02658-4_39.
    • Jones, Neil D., und Müller-Olm, Markus, Hrsg. . Lecture Notes in Computer Science, Bd. 5403, Verification, Model Checking, and Abstract Interpretation, Düsseldorf: Springer VDI Verlag. doi: 10.1007/978-3-540-93900-9.
    • , und . . „Conflict analysis of programs with procedures, dynamic thread creation, and monitors.“ In Static analysis, Bd. 5079 aus Lecture Notes in Computer Science, herausgegeben von Vidal Germán Alpuente María. Heidelberg: Springer. doi: 10.1007/978-3-540-69166-2_14.
    • , und . . „Upper adjoints for fast inter-procedural variable equalities.“ In Programming Languages and Systems, Bd. 4960 aus Lecture Notes in Computer Science, herausgegeben von Drossopoulou Sophia. Heidelberg: Springer. doi: 10.1007/978-3-540-78739-6_15.
    • , und . . „Analysis of modular arithmetic.“ ACM Transactions on Programming Languages and Systems, Nr. 29 (5) doi: 10.1145/1275497.1275504.
    • , und . . „Precise fixpoint-based analysis of programs with thread-creation and procedures.“ In CONCUR 2007 - Concurrency Theory, Bd. 4703 aus Lecture Notes in Computer Science, herausgegeben von Vasconcelos Vasco T. Caires Luís. Heidelberg: Springer. doi: 10.1007/978-3-540-74407-8_20.
    • , , und . . „Interprocedurally analyzing polynomial identities.“ In STACS 2006, Bd. 3884 aus Lecture Notes in Computer Science, herausgegeben von Thomas Wolfgang Durand Bruno. Heidelberg: Springer. doi: 10.1007/11672142_3.
    • . . Lecture Notes in Computer Science, Bd. 3800, Variations on Constants: Flow Analysis of Sequential and Parallel Programs, Düsseldorf: Springer VDI Verlag. doi: 10.1007/11871743.
    • , und . . „A generic framework for interprocedural analysis of numerical properties.“ In Static Analysis, Bd. 3672 aus Lecture Notes in Computer Science, herausgegeben von Siveroni Igor Hankin Chris. Heidelberg: Springer. doi: 10.1007/11547662_17.
    • , , und . . „Regular symbolic analysis of dynamic networks of pushdown systems.“ In CONCUR 2005 - Concurrency Theory, Bd. 3653 aus Lecture Notes in Computer Science, herausgegeben von de Alfaro Luca Abadi Martín. Heidelberg: Springer. doi: 10.1007/11539452_36.
    • , , und . . „Checking Herbrand equalities and beyond.“ In Verification, Model Checking, and Abstract Interpretation, Bd. 3385 aus Lecture Notes in Computer Science, herausgegeben von Cousot Radhia. Heidelberg: Springer. doi: 10.1007/978-3-540-30579-8_6.
    • , und . . „Analysis of modular arithmetic.“ In Programming Languages and Systems, Bd. 3444 aus Lecture Notes in Computer Science, herausgegeben von Sagiv Mooly. Heidelberg: Springer. doi: 10.1007/978-3-540-31987-0_5.
    • , , und . . „Interprocedural Herbrand equalities.“ In Programming Languages and Systems, Bd. 3444 aus Lecture Notes in Computer Science, herausgegeben von Sagiv Mooly. Heidelberg: Springer. doi: 10.1007/978-3-540-31987-0_4.
    • . . „Precise interprocedural analysis through linear algebra.“ In Conference Record of the 31st Annual ACM Symposium on Principles of Programming Languages, herausgegeben von Neil D. Jones und Xavier Leroy. New York, NY: ACM Press.
    • , und . . „A note on Karr's algorithm.“ In Automata, Languages and Programming, Bd. 3142 aus Lecture Notes in Computer Science, herausgegeben von Karhumäki Juhani Díaz Josep und Sannella Donald Lepistö Arto. Heidelberg: Springer. doi: 10.1007/978-3-540-27836-8_85.
    • , und . . „Formal development and verification of approximation algorithms using auxiliary variables.“ In Logic based program synthesis and transformation: Revised Selected Papers, Bd. 3018 aus Lecture Notes in Computer Science, herausgegeben von Maurice Bruynooghe. Heidelberg: Springer. doi: 10.1007/978-3-540-25938-1_6.
    • , und . . „Computing polynomial program invariants.“ Information Processing Letters, Nr. 91 (5): 233–244. doi: 10.1016/j.ipl.2004.05.004.
    • . . „Precise interprocedural dependence analysis of parallel programs.“ Theoretical Computer Science, Nr. 311 (1-3): 325–388. doi: 10.1016/j.tcs.2003.09.002.
    • , und . . „MetaGame: An animation tool for model-checking games.“ In Tools and Algorithms for the Construction and Analysis of Systems, Bd. 2988 aus Lecture Notes in Computer Science, herausgegeben von Podelski Andreas Jensen Kurt. Heidelberg: Springer. doi: 10.1007/978-3-540-24730-2_14.
    • , , und . . „Global invariants for analysing multi-threaded applications.“ Proceedings of the Estonian Academy of Sciences: Physics Mathematics, Nr. 52 (4): 413–436.
    • , und . . „Polynomial constants are decidable.“ In Static Analysis, Bd. 2477 aus Lecture Notes in Computer Science, herausgegeben von Manuel V. Hermenegildo und Germán Puebla. Heidelberg: Springer. doi: 10.1007/3-540-45789-5_4.
    • , und . . „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, herausgegeben von Vitter Scott, Spirakis G. und Yannakakis Mihalis. New York, NY: ACM Press. doi: 10.1145/380752.380864.
    • . . „The complexity of copy constant detection in parallel programs.“ In STACS 2001, Bd. 2010 aus Lecture Notes in Computer Science, herausgegeben von Reichel Horst Ferreira Afonso. Heidelberg: Springer. doi: 10.1007/3-540-44693-1_43.
    • , und . . „On the complexity of constant propagation.“ In Programming Languages and Systems, Bd. 2028 aus Lecture Notes in Computer Science, herausgegeben von Sands David. Heidelberg: Springer. doi: 10.1007/3-540-45309-1_13.
    • , und . . „On the translation of procedures to finite machines.“ In Programming Languages and Systems, Bd. 1782 aus Lecture Notes in Computer Science, herausgegeben von Smolka Gert. Heidelberg: Springer. doi: 10.1007/3-540-46425-5_19.
    • . . „A modal fixpoint logic with chop.“ In STACS 99, Bd. 1563 aus Lecture Notes in Computer Science, herausgegeben von Tison Sophie Meinel Christoph. Heidelberg: Springer. doi: 10.1007/3-540-49116-3_48.
    • , , , und . . „Beyond ProCoS at Kiel: A synopsis of recent research.“ Beitrag präsentiert auf der ProCoS WG workshop at FM'99, Toulouse, France Heidelberg: Springer.
    • , und . . „Compilation and synthesis for real-time embedded controllers.“ In Correct System Design, Bd. 1710 aus Lecture Notes in Computer Science, herausgegeben von Steffen Bernhard Olderog Ernst-Rüdiger. Düsseldorf: Springer VDI Verlag. doi: 10.1007/3-540-48092-7_12.
    • , , und . . „Model-checking: A tutorial introduction.“ In Static Analysis, Bd. 1694 aus Lecture Notes in Computer Science, herausgegeben von Filé Gilberto Cortesi Agostino. Heidelberg: Springer. doi: 10.1007/3-540-48294-6_22.
    • , und . . „On excusable and inexcusable failures: Towards an adequate notion of translation correctness.“ In FM’99 — Formal Methods, Bd. 1709 aus Lecture Notes in Computer Science, herausgegeben von Wing M., Woodcock Jim und Davies Jim. Heidelberg: Springer. doi: 10.1007/3-540-48118-4_9.
    • , , und . . „On the evolution of reactive components.“ In Fundamental Approaches to Software Engineering, Bd. 1577 aus Lecture Notes in Computer Science, herausgegeben von Finance Jean-Pierre. Heidelberg: Springer. doi: 10.1007/978-3-540-49020-3_11.
    • . . „Derivation of characteristic formulae.“ In Proc. MFCS'98 Workshop on Concurrency, Bd. 18 aus Electronic Notes in Theoretical Computer Science, herausgegeben von Kretinsky Mojmir Jancar Petr. Amsterdam: Elsevier. doi: 10.1016/S1571-0661(05)80257-9.
    • . . Lecture Notes in Computer Science, Bd. 1283, Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, Düsseldorf: Springer VDI Verlag. doi: 10.1007/BFb0027453.
    • , und . . „Towards provably correct code generation for a hard real-time programming language.“ In Compiler Construction, Bd. 786 aus Lecture Notes in Computer Science, herausgegeben von Fritzson A.. Heidelberg: Springer. doi: 10.1007/3-540-57877-3_20.
    • , , , , , , , , und . „Provably correct systems.“ In Formal Techniques in Real-Time and Fault-Tolerant Systems, Bd. 863 aus Lecture Notes in Computer Science, herausgegeben von H. Langmaack, W.-P. de Roever und J. Vytopil. Heidelberg: Springer. doi: 10.1007/3-540-58468-4_171.
    • , , , , , , und . . „Provably correct compiler development and implementation.“ In Compiler Construction, Bd. 641 aus Lecture Notes in Computer Science, herausgegeben von Pfahler Peter Kastens Uwe. Heidelberg: Springer. doi: 10.1007/3-540-55984-1_14.

  • Betreute Promotionen

    Lock-Sensitive Reachability Analysis for Parallel Recursive Programs with Dynamic Creation of Threads and Locks
    Security Through Safety: An Approach to Information Flow Control Based on Derivation of Safety Properties From a Characterisation of Insecure Behavior
    Meuth, PatrickThalamische Neurone in silico
    Locksensitive Analyse paralleler Programme