Dominik Klumpp
 |
Dominik Klumpp
University of FreiburgGeorges-Köhler-Allee 52
79110 Freiburg
building 052, room 00-022 klumpp@informatik.uni-freiburg.de Homepage: dominik-klumpp.net
|
Research Interests
automatic verification, concurrent programs, commutativity / partial order reduction
Publications & Talks
DBLP -- ORCID -- ResearchGate -- Google Scholar -- FreiDok
- Walking the Tightrope between Expressiveness and Uncomputability: AGM Contraction beyond the Finitary Realm, in NMR 2024, together with Jandson S. Ribeiro [link] [extended version]
- Ultimate Automizer and the Abstraction of Bitwise Operations, in TACAS 2024 (SV-COMP'24), together with Frank Schüssele, Manuel Bentele, Daniel Dietsch, Matthias Heizmann, Xinyu Jiang, and Andreas Podelski [doi]
- 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. [doi] [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, 2022, 2024)
In the summer semester 2024, I was the lecturer for this course. - 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 | Combination Operators for Monitor-Based Preference Orders | ongoing |
| MSc Project | Computing omega-Reductions with Ample Sets | ongoing |
| BSc Thesis | Translating YAML correctness witnesses for deductive verifiers | ongoing |
| BSc Thesis | Constructing Empire Annotations from Petri Nets | 2024 |
| BSc Thesis | Büchi-Mealy Contraction and the Maximal Cut Property | 2024 |
| MSc Thesis | Investigating Conditional Commutativity for Concurrent Program Verification | 2024 |
| BSc Project | Computing Small Proofs for Concurrent Programs | 2024 |
| BSc Project | Stratified Source Sets | 2023 |
| 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 | 2023 |
| 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.