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
- . . ‘Automata and Fixpoints for Asynchronous Hyperproperties.’ Proc. ACM Program. Lang. (POPL) 5, Nr. POPL: 1–29. doi: 10.1145/3434319.
- . . ‘Temporal Logics with Language Parameters.’ In Language and Automata Theory and Applications - 15th International Conference, LATA 2021, Milan, Italy, March 1-5, 2021, Proceedings, edited by , 187–199.: Springer. doi: 10.1007/978-3-030-68195-1\_14.
- . . ‘Propositional Dynamic Logic for Hyperproperties.’ In 31st International Conference on Concurrency Theory, edited by .: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi: 10.4230/LIPIcs.CONCUR.2020.50.
- (Eds.): . 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.
- . . ‘A Branching Time Variant of CaRet.’ In Model Checking Software - 25th International Symposium, SPIN 2018, edited by , 153–170.: Springer. doi: 10.1007/978-3-319-94111-0\_9.
- . . ‘Using Dynamic Pushdown Networks to Automate a Modular Information-flow Analysis.’ In Logic-Based Program Synthesis and Transformation, edited by .: Springer International Publishing. doi: 10.1007/978-3-319-27436-2_12.
- (Eds.): . 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.
- . . ‘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 , 384–403. Manhattan, Kansas, USA: Open Publishing Association. doi: 10.4204/EPTCS.129.24.
- . . ‘Contextual Locking for Dynamic Pushdown Networks.’ In 20th Static Analysis Symposium, edited by , 477–498.: Springer.
- . . ‘Fast interprocedural linear two variable equalities.’ ACM Transactions on Programming Languages and Systems 33, Nr. 6.
- . . ‘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.
- (Eds.): . Tagungsband 16. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'11). Münster: Institut für Wirtschaftsinformatik.
- . . ‘Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation.’ In Verification, Model Checking and Abstract Interpretation, edited by , 199–213. Berlin, Heidelberg, New York: Springer-Verlag. doi: 10.1007/978-3-642-18275-4_15.
- . . ‘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 , 93–104.: ACM. doi: 10.1145/1926385.1926398.
- . . ‘Predecessor sets of dynamic pushdown networks with tree-regular constraints.’ In Computer Aided Verification, edited by , 525–539.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-642-02658-4_39.
- (Eds.): . Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg, New York: Springer VDI Verlag. doi: 10.1007/978-3-540-93900-9.
- . . ‘Conflict analysis of programs with procedures, dynamic thread creation, and monitors.’ In Static analysis, edited by , 205–220. Berlin: Springer. doi: 10.1007/978-3-540-69166-2_14.
- . . ‘Upper adjoints for fast inter-procedural variable equalities.’ In Programming Languages and Systems, edited by , 178–192.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-78739-6_15.
- . . ‘Analysis of modular arithmetic.’ ACM Transactions on Programming Languages and Systems 29, Nr. 5. doi: 10.1145/1275497.1275504.
- . . ‘Precise fixpoint-based analysis of programs with thread-creation and procedures.’ In CONCUR 2007 - Concurrency Theory, edited by , 287–302. Berlin: Springer. doi: 10.1007/978-3-540-74407-8_20.
- . . ‘Interprocedurally analyzing polynomial identities.’ In STACS 2006, edited by , 50–67. Berlin: Springer. doi: 10.1007/11672142_3.
- . . Variations on Constants: Flow Analysis of Sequential and Parallel Programs. Berlin, Heidelberg, New York: Springer VDI Verlag. doi: 10.1007/11871743.
- . . ‘A generic framework for interprocedural analysis of numerical properties.’ In Static Analysis, edited by , 235–250. Berlin: Springer. doi: 10.1007/11547662_17.
- . . ‘Regular symbolic analysis of dynamic networks of pushdown systems.’ In CONCUR 2005 - Concurrency Theory, edited by , 473–487. Berlin: Springer. doi: 10.1007/11539452_36.
- . . ‘Checking Herbrand equalities and beyond.’ In Verification, Model Checking, and Abstract Interpretation, edited by , 79–96. Berlin: Springer. doi: 10.1007/978-3-540-30579-8_6.
- . . ‘Analysis of modular arithmetic.’ In Programming Languages and Systems, edited by , 46–60.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-31987-0_5.
- . . ‘Interprocedural Herbrand equalities.’ In Programming Languages and Systems, edited by , 31–45.: Springer Berlin / Heidelberg. 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, edited by , 330–341.: ACM.
- . . ‘A note on Karr's algorithm.’ In Automata, Languages and Programming, edited by , 1016–1028. Berlin: Springer. doi: 10.1007/978-3-540-27836-8_85.
- . . ‘Formal development and verification of approximation algorithms using auxiliary variables.’ In Logic based program synthesis and transformation: Revised Selected Papers, edited by , 59–74. Berlin: Springer. doi: 10.1007/978-3-540-25938-1_6.
- . . ‘Computing polynomial program invariants.’ Information Processing Letters 91, Nr. 5: 233–244. doi: 10.1016/j.ipl.2004.05.004.
- . . ‘Precise interprocedural dependence analysis of parallel programs.’ Theoretical Computer Science 311, Nr. 1-3: 325–388. doi: 10.1016/j.tcs.2003.09.002.
- . . ‘MetaGame: An animation tool for model-checking games.’ In Tools and Algorithms for the Construction and Analysis of Systems, edited by , 163–167.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-24730-2_14.
- . . ‘Global invariants for analysing multi-threaded applications.’ Proceedings of the Estonian Academy of Sciences: Physics Mathematics 52, Nr. 4: 413–436.
- . . ‘Polynomial constants are decidable.’ In Static Analysis, edited by , 4–19. Berlin: Springer. doi: 10.1007/3-540-45789-5_4.
- . . ‘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 , 647–656. New York: ACM. doi: 10.1145/380752.380864.
- . . ‘The complexity of copy constant detection in parallel programs.’ In STACS 2001, edited by , 490–501.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-44693-1_43.
- . . ‘On the complexity of constant propagation.’ In Programming Languages and Systems, edited by , 190–205.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-45309-1_13.
- . . ‘On the translation of procedures to finite machines.’ In Programming Languages and Systems, edited by , 290–304.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-46425-5_19.
- . . ‘A modal fixpoint logic with chop.’ In STACS 99, edited by , 510–520. Berlin: Springer. doi: 10.1007/3-540-49116-3_48.
- . . ‘Beyond ProCoS at Kiel: A synopsis of recent research.’ Contributed to the ProCoS WG workshop at FM'99, Toulouse, France.
- . . ‘Compilation and synthesis for real-time embedded controllers.’ In Correct System Design, edited by , 256–287. Springer VDI Verlag. doi: 10.1007/3-540-48092-7_12.
- . . ‘Model-checking: A tutorial introduction.’ In Static Analysis, edited by , 330–354.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-48294-6_22.
- . . ‘On excusable and inexcusable failures: Towards an adequate notion of translation correctness.’ In FM’99 — Formal Methods, edited by , 1107–1127.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-48118-4_9.
- . . ‘On the evolution of reactive components.’ In Fundamental Approaches to Software Engineering, edited by , 161–175.: Springer Berlin / Heidelberg. doi: 10.1007/978-3-540-49020-3_11.
- . . ‘Derivation of characteristic formulae.’ In Proc. MFCS'98 Workshop on Concurrency, edited by , 159–170. Amsterdam: Elsevier. doi: 10.1016/S1571-0661(05)80257-9.
- . . Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction. Berlin, Heidelberg, New York: Springer VDI Verlag. doi: 10.1007/BFb0027453.
- . . ‘Towards provably correct code generation for a hard real-time programming language.’ In Compiler Construction, edited by , 294–308.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-57877-3_20.
- . ‘Provably correct systems.’ In Formal Techniques in Real-Time and Fault-Tolerant Systems, edited by , 288–335.: Springer Berlin / Heidelberg. doi: 10.1007/3-540-58468-4_171.
- . . ‘Provably correct compiler development and implementation.’ In Compiler Construction, edited by , 141–155.: Springer Berlin / Heidelberg. 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
Professur für Praktische Informatik (Prof. Müller-Olm)
