You are here: Home Team Dominik Klumpp

Dominik Klumpp

 

Research Interests

automatic verification, concurrent programs, partial order reduction, control flow

Publications & Talks

DBLP -- ORCID -- ResearchGate -- Google Scholar -- FreiDok

  • Commutativity Simplifies Proofs of Parameterized Programs, in POPL 2024, together with Azadeh Farzan and Andreas Podelski. [doi] [preprint]
  • Petrification: Software Model Checking for Programs with Dynamic Thread Management, in VMCAI 2024, together with Matthias Heizmann, Lars Nitzke and Frank Schüssele. [preprint]
  • Ultimate Taipan and Race Detection in Ultimate, in TACAS 2023 (SV-COMP'23), together with Daniel Dietsch, Matthias Heizmann, Frank Schüssele and Andreas Podelski. [doi]
  • Ultimate Automizer and the CommuHash Normal Form, in TACAS 2023 (SV-COMP'23), together with Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Mehdi Naouar, Tanja Schindler, Frank Schüssele and Andreas Podelski. [doi]
  • Stratified Commutativity in Verification Algorithms for Concurrent Programs, in POPL 2023, together with Azadeh Farzan and Andreas Podelski. [doi] [Slides] [Talk]
  • (Talk & Poster) Commutativity in Concurrent Program Verification, at FMCAD 2022 [Slides][Poster]
  • (Talk) Commutativity in Concurrent Program Verification, at AVM 2022 [Slides]
  • (Talk) Extending Commutativity via Safe Abstraction, in Commute 2022 [Slides]
  • Sound Sequentialization for Concurrent Program Verification, in PLDI 2022, together with Azadeh Farzan and Andreas Podelski. [doi] [Slides] [Talk]
  • Ultimate GemCutter and the Axes of Generalization, in TACAS 2022 (SV-COMP'22), together with Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan and Andreas Podelski. [doi] [Slides]
  • Verification of Concurrent Programs Using Petri Net Unfoldings, in VMCAI 2021, together with Daniel Dietsch, Matthias Heizmann, Mehdi Naouar, Andreas Podelski and Claus Schätzle. [doi] [Slides] [Talk]
  • (Talk) Partial Order Reduction for Trace Abstraction Refinement, in MOVEP 2020 [Extended Abstract] [Slides]
  • 𝕂 and KIV: Towards Deductive Verification for Arbitrary Programming Languages, in WADT 2020, together with Philip Lenzen. [doi] [Slides] [Poster]
  • Automated Control Flow Reconstruction from Assembler Programs, MSc Thesis (2018) at the University of Augsburg. [doi] [Slides from AVM'19] [
  • Measuring and Evaluating the Performance of Self-Organization Mechanisms Within Collective Adaptive Systems, in ISOLA 2018, together with Benedikt Eberhardinger, Hella Ponsar and Wolfgang Reif. [doi]
  • Test Case Selection Strategy for Self-Organization Mechanisms, in Test, Analyse und Verifikation von Software – gestern, heute, morgen, together with Benedikt Eberhardinger, Hella Ponsar and Wolfgang Reif.
  • Optimising Runtime Safety Analysis Efficiency for Self-Organising Systems, in FAS*/QA4SASO 2016, together with Axel Habermaier, Benedikt Eberhardinger and Hella Seebach. [doi]

Lectures & Seminars

I co-organise the following lectures:

  • Cyber-Physical Systems: Discrete Models (in the winter semester 2019/20, 2020/21, 2021/22 and 2022/23)
  • Cyber-Physical Systems: Program Verification (in the summer semesters 2019, 2020, 2021 and 2022)
  • Theoretische Informatik (in the summer semesters 2022 and 2023)

I supervise students in the BSc Proseminar "Klassische Artikel der Programmanalyse" (2019/2020 and 2020/2021), the BSc Proseminar/Seminar "Automata Theory" (2020, 2021, 2022/2023) and the MSc Seminar "Advanced Topics in Program Analysis" (2020/2021).

Project Supervisions

BSc Project Computing Small Proofs for Concurrent Programs ongoing
BSc Project Stratified Source Sets ongoing
BSc Thesis Stratified Reduction with Dynamic Abstractions 2023
BSc Thesis Dynamic Partial Order Reduction on Tree-shaped Automata for Verification of Concurrent Programs 2023
MSc Project Selecting Preference Orders ongoing
MSc Thesis Computing Representative Automata for Maximal Causality Reduction 2022
MEd Project Statement Abstraction for POR 2022
MSc Thesis Owicki-Gries Correctness Proofs from Petri Net Unfoldings 2021
MSc Project Trace Abstraction Refinement with Repeated Lipton Reduction 2021
BSc Thesis Tight integration of Partial Order Reduction into Trace Abstraction Refinement 2021
MSc Project Owicki-Gries Correctness Proof Scheme 2020
MSc Thesis Clinical Guidelines Verification with ULTIMATE: A Case-Study Approach 2020
MSc Thesis Trace Abstraction with Maximal Causality Reduction 2020
BSc Thesis Large Block Encoding for Concurrent Programs 2019

 

If you are interested in a project or thesis, send me an email. See here for some topic ideas, or bring your own.

Consultation Hours

Please send me an e-mail to make an appointment.