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
- Gutsfeld, Jens Oliver, Müller-Olm, Markus, und Ohrem, Christoph. . „Automata and Fixpoints for Asynchronous Hyperproperties.“ Proc. ACM Program. Lang. (POPL) POPL), Nr. 5 : 1–29. doi: 10.1145/3434319.
- Gutsfeld, Jens Oliver, Müller-Olm, Markus, und Dielitz, Christian. . „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 Alberto Leporati, Carlos Martı́n-Vide und Dana Zandron Claudio Shapira. Springer. doi: 10.1007/978-3-030-68195-1\_14.
- Gutsfeld, Jens, Müller-Olm, Markus, und Ohrem, Christoph. . „Propositional Dynamic Logic for Hyperproperties.“ In 31st International Conference on Concurrency Theory, Bd. 171 aus LIPIcs, herausgegeben von Igor Konnov und Laura Kovács. Dagstuhl Publishing. doi: 10.4230/LIPIcs.CONCUR.2020.50.
- Feng, Xinyu, Müller-Olm, Markus, und Yang, Zijiang, Hrsg. . Lecture Notes in Computer Science, Bd. 10998, Dependable Software Engineering. Theories, Tools, and Applications - 4th International Symposium, SETTA 2018, Beijing, China Springer VDI Verlag. doi: 10.1007/978-3-319-99933-3.
- Gutsfeld, Jens, Müller-Olm, Markus, und Nordhoff, Benedikt. . „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 María-del-Mar Gallardo und Pedro Merino. Springer. doi: 10.1007/978-3-319-94111-0\_9.
- Mantel, Heiko, Müller-Olm, Markus, Perner, Matthias, und Wenner, Alexander. . „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. Springer International Publishing. doi: 10.1007/978-3-319-27436-2_12.
- Müller-Olm, Markus Seidl Helmut, Hrsg. . Lecture Notes in Computer Science, Bd. 8723, Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings Springer VDI Verlag. doi: 10.1007/978-3-319-10936-7.
- Nordhoff, Benedikt, Müller-Olm, Markus, und Lammich, Peter. . „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. Manhattan, Kansas, USA: Open Publishing Association. doi: 10.4204/EPTCS.129.24.
- Lammich, Peter, Müller-Olm, Markus, Seidl, Helmut, und Wenner, Alexander. . „Contextual Locking for Dynamic Pushdown Networks.“ In 20th Static Analysis Symposium, Bd. 7935 aus Lecture Notes in Computer Science, herausgegeben von Logozzo Francesco und Fahndrich Manuel. Springer.
- Flexeder, Andrea, Müller-Olm, Markus, Petter, Michael, und Seidl, Helmut. . „Fast interprocedural linear two variable equalities.“ ACM Transactions on Programming Languages and Systems 6), Nr. 33
- Jones, Neil D., und Müller-Olm, Markus. . „Preface to a special section on verification, model checking, and abstract interpretation.“ International Journal on Software Tools for Technology Transfer 6), Nr. 13 : 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.
- Gawlitza, Thomas, Lammich, Peter, Müller-Olm, Markus, Seidl, Helmut, und Wenner, Alexander. . „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 Ranjit Jhala und David Schmidt. Berlin, Heidelberg, New York: Springer. doi: 10.1007/978-3-642-18275-4_15.
- Schwarz, Martin D, Seidl, Helmut, Vojdani, Vesal, Lammich, Peter, und Müller-Olm, Markus. . „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 Thomas Ball und Mooly Sagiv. ACM Press. doi: 10.1145/1926385.1926398.
- Lammich, Peter, Müller-Olm, Markus, und Wenner, Alexander. . „Predecessor sets of dynamic pushdown networks with tree-regular constraints.“ In Computer Aided Verification, Bd. 5643 aus Lecture Notes in Computer Science, herausgegeben von Ahmed Bouajjani und Oded Maler. 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 Berlin, Heidelberg, New York: Springer VDI Verlag. doi: 10.1007/978-3-540-93900-9.
- Lammich, Peter Müller-Olm Markus. . „Conflict analysis of programs with procedures, dynamic thread creation, and monitors.“ In Static analysis, Bd. 5079 aus Lecture Notes in Computer Science, herausgegeben von María Alpuente und Germán Vidal. Berlin: Springer. doi: 10.1007/978-3-540-69166-2_14.
- Müller-Olm, Markus Seidl Helmut. . „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. Springer. doi: 10.1007/978-3-540-78739-6_15.
- Müller-Olm, Markus Seidl Helmut. . „Analysis of modular arithmetic.“ ACM Transactions on Programming Languages and Systems 5), Nr. 29 doi: 10.1145/1275497.1275504.
- Lammich, Peter Müller-Olm Markus. . „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 Luís Caires und Vasco T. Vasconcelos. Berlin: Springer. doi: 10.1007/978-3-540-74407-8_20.
- Müller-Olm, Markus, Petter, Michael, und Seidl, Helmut. . „Interprocedurally analyzing polynomial identities.“ In STACS 2006, Bd. 3884 aus Lecture Notes in Computer Science, herausgegeben von Bruno Durand und Wolfgang Thomas. Berlin: Springer. doi: 10.1007/11672142_3.
- Müller-Olm, Markus. . Lecture Notes in Computer Science, Bd. 3800, Variations on Constants: Flow Analysis of Sequential and Parallel Programs Berlin, Heidelberg, New York: Springer VDI Verlag. doi: 10.1007/11871743.
- Müller-Olm, Markus Seidl Helmut. . „A generic framework for interprocedural analysis of numerical properties.“ In Static Analysis, Bd. 3672 aus Lecture Notes in Computer Science, herausgegeben von Chris Hankin und Igor Siveroni. Berlin: Springer. doi: 10.1007/11547662_17.
- Bouajjani, Ahmed, Müller-Olm, Markus, und Touili, Tayssir. . „Regular symbolic analysis of dynamic networks of pushdown systems.“ In CONCUR 2005 - Concurrency Theory, Bd. 3653 aus Lecture Notes in Computer Science, herausgegeben von Martín Abadi und Alfaro Luca de. Berlin: Springer. doi: 10.1007/11539452_36.
- Müller-Olm, Markus, Rüthing, Oliver, und Seidl, Helmut. . „Checking Herbrand equalities and beyond.“ In Verification, Model Checking, and Abstract Interpretation, Bd. 3385 aus Lecture Notes in Computer Science, herausgegeben von Cousot Radhia. Berlin: Springer. doi: 10.1007/978-3-540-30579-8_6.
- Müller-Olm, Markus Seidl Helmut. . „Analysis of modular arithmetic.“ In Programming Languages and Systems, Bd. 3444 aus Lecture Notes in Computer Science, herausgegeben von Sagiv Mooly. Springer. doi: 10.1007/978-3-540-31987-0_5.
- Müller-Olm, Markus, Seidl, Helmut, und Steffen, Bernhard. . „Interprocedural Herbrand equalities.“ In Programming Languages and Systems, Bd. 3444 aus Lecture Notes in Computer Science, herausgegeben von Sagiv Mooly. Springer. doi: 10.1007/978-3-540-31987-0_4.
- Müller-Olm, Markus, und Seidl, Helmut. . „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. ACM Press.
- Müller-Olm, Markus Seidl Helmut. . „A note on Karr's algorithm.“ In Automata, Languages and Programming, Bd. 3142 aus Lecture Notes in Computer Science, herausgegeben von Josep Díaz, Juhani Karhumäki, Arto Lepistö und Donald Sannella. Berlin: Springer. doi: 10.1007/978-3-540-27836-8_85.
- Berghammer, Rudolf Müller-Olm Markus. . „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. Berlin: Springer. doi: 10.1007/978-3-540-25938-1_6.
- Müller-Olm, Markus Seidl Helmut. . „Computing polynomial program invariants.“ Information Processing Letters 5), Nr. 91 : 233–244. doi: 10.1016/j.ipl.2004.05.004.
- Müller-Olm, Markus. . „Precise interprocedural dependence analysis of parallel programs.“ Theoretical Computer Science 1-3), Nr. 311 : 325–388. doi: 10.1016/j.tcs.2003.09.002.
- Müller-Olm, Markus Yoo Haiseung. . „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 Kurt Jensen und Andreas Podelski. Springer. doi: 10.1007/978-3-540-24730-2_14.
- Seidl, Helmut, Vene, Varmo, und Müller-Olm, Markus. . „Global invariants for analysing multi-threaded applications.“ Proceedings of the Estonian Academy of Sciences: Physics Mathematics 4), Nr. 52 : 413–436.
- Müller-Olm, Markus Seidl Helmut. . „Polynomial constants are decidable.“ In Static Analysis, Bd. 2477 aus Lecture Notes in Computer Science, herausgegeben von Manuel V. Hermenegildo und Germán Puebla. Berlin: Springer. doi: 10.1007/3-540-45789-5_4.
- Müller-Olm, Markus Seidl Helmut. . „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 Jeffrey Scott Vitter, Paul G. Spirakis und Mihalis Yannakakis. New York: ACM Press. doi: 10.1145/380752.380864.
- Müller-Olm, Markus. . „The complexity of copy constant detection in parallel programs.“ In STACS 2001, Bd. 2010 aus Lecture Notes in Computer Science, herausgegeben von Afonso Ferreira und Horst Reichel. Springer. doi: 10.1007/3-540-44693-1_43.
- Müller-Olm, Markus Rüthing Oliver. . „On the complexity of constant propagation.“ In Programming Languages and Systems, Bd. 2028 aus Lecture Notes in Computer Science, herausgegeben von Sands David. Springer. doi: 10.1007/3-540-45309-1_13.
- Müller-Olm, Markus Wolf Andreas. . „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. Springer. doi: 10.1007/3-540-46425-5_19.
- Müller-Olm, Markus. . „A modal fixpoint logic with chop.“ In STACS 99, Bd. 1563 aus Lecture Notes in Computer Science, herausgegeben von Christoph Meinel und Sophie Tison. Berlin: Springer. doi: 10.1007/3-540-49116-3_48.
- Fränzle, Martin Goerigk Wolfgang, und von Karger Burghard, Müller-Olm Markus. . „Beyond ProCoS at Kiel: A synopsis of recent research.“ Beitrag präsentiert auf der ProCoS WG workshop at FM'99, Toulouse, France FM'99 CD-Rom: Springer.
- Fränzle, Martin Müller-Olm Markus. . „Compilation and synthesis for real-time embedded controllers.“ In Correct System Design, Bd. 1710 aus Lecture Notes in Computer Science, herausgegeben von Ernst-Rüdiger Olderog und Bernhard Steffen. Springer VDI Verlag. doi: 10.1007/3-540-48092-7_12.
- Müller-Olm, Markus, Schmidt, David, und Steffen, Bernhard. . „Model-checking: A tutorial introduction.“ In Static Analysis, Bd. 1694 aus Lecture Notes in Computer Science, herausgegeben von Agostino Cortesi und Gilberto Filé. Springer. doi: 10.1007/3-540-48294-6_22.
- Müller-Olm, Markus Wolf Andreas. . „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 Jeanette M. Wing, Jim Woodcock und Jim Davies. Springer. doi: 10.1007/3-540-48118-4_9.
- Müller-Olm, Markus, Steffen, Bernhard, und Cleaveland, Ramce. . „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. Springer. doi: 10.1007/978-3-540-49020-3_11.
- Müller-Olm, Markus. . „Derivation of characteristic formulae.“ In Proc. MFCS'98 Workshop on Concurrency, Bd. 18 aus Electronic Notes in Theoretical Computer Science, herausgegeben von Petr Jancar und Mojmir Kretinsky. Amsterdam: Elsevier. doi: 10.1016/S1571-0661(05)80257-9.
- Müller-Olm, Markus. . Lecture Notes in Computer Science, Bd. 1283, Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction Berlin, Heidelberg, New York: Springer VDI Verlag. doi: 10.1007/BFb0027453.
- Fränzle, Martin Müller-Olm Markus. . „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 Peter A.. Springer. doi: 10.1007/3-540-57877-3_20.
- He, J., Hoare, C.A.R., Fränzle, M., Müller-Olm, M., Olderog, E.-R., Schenke, M., Hansen, M., Ravn, A., und Rischel, H. . „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. Springer. doi: 10.1007/3-540-58468-4_171.
- Buth, Bettina, Buth, Karl-Heinz, Fränzle, Martin, Burghard, von Karger, Lakhneche, Yassine, Langmaack, Hans, und Müller-Olm, Markus. . „Provably correct compiler development and implementation.“ In Compiler Construction, Bd. 641 aus Lecture Notes in Computer Science, herausgegeben von Uwe Kastens und Peter Pfahler. Springer. doi: 10.1007/3-540-55984-1_14.
Betreute Promotionen
Kenter, Sebastian Lock-Sensitive Reachability Analysis for Parallel Recursive Programs with Dynamic Creation of Threads and Locks Nordhoff, Benedikt Security Through Safety: An Approach to Information Flow Control Based on Derivation of Safety Properties From a Characterisation of Insecure Behavior Meuth, Patrick Thalamische Neurone in silico Lammich, Peter Locksensitive Analyse paralleler Programme
Prof. Dr. Markus Müller-Olm
