Publications

full bibliography (BibTeX)

• Ultimate Automizer and the Abstraction of Bitwise Operations SV-COMP@ETAPS'24
  

  Authors: Frank Schüssele, Manuel Bentele, Daniel Dietsch, Matthias Heizmann, Xinyu Jiang, Dominik Klumpp, Andreas Podelski

  Springer Artifact

  The verification of Ultimate Automizer works on an SMT-LIB-based model of a C program. If we choose an SMT-LIB theory of (mathematical) integers, the translation is not precise, because we overapproximate bitwise operations. In this paper we present a translation for bitwise operations that improves the precision of this overapproximation.

  @inproceedings{tacas24:ultimateAutomizer,
    author    = {Frank Sch{\"{u}}ssele and Manuel Bentele and Daniel Dietsch and Matthias Heizmann and Xinyu Jiang and Dominik Klumpp and Andreas Podelski},
    title     = {Ultimate Automizer and the Abstraction of Bitwise Operations (Competition Contribution)},
    booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
                 - 30th International Conference, {TACAS} 2024, Held as Part of the
                 European Joint Conferences on Theory and Practice of Software, {ETAPS}
                 2024, Luxembourg, Luxembourg, April 08-11, 2024, Proceedings, Part {II}},
    publisher = {Springer},
    year      = {2024},
    doi       = {10.1007/978-3-031-57256-2\_31}
  }

• Commutativity Simplifies Proofs of Parameterized Programs POPL'24
  

  Authors: Azadeh Farzan, Dominik Klumpp, Andreas Podelski

  ACM Preprint (arxiv) Slides Recording Artifact

  Commutativity has proven to be a powerful tool in reasoning about concurrent programs. Recent work has shown that a commutativity-based reduction of a program may admit simpler proofs than the program itself. The framework of lexicographical program reductions was introduced to formalize a broad class of reductions which accommodate sequential (thread-local) reasoning as well as synchronous programs. Approaches based on this framework, however, were fundamentally limited to program models with a fixed/bounded number of threads. In this paper, we show that it is possible to define an effective parametric family of program reductions that can be used to find simple proofs for parameterized programs, i.e., for programs with an unbounded number of threads. We show that reductions are indeed useful for the simplification of proofs of parameterized programs, in a sense that can be made precise: A reduction of a parameterized program may admit a proof which uses fewer or less sophisticated ghost variables. The reduction may therefore be within reach of an automated verification technique, even when the original parameterized program is not. As our first technical contribution, we introduce a notion of reductions for parameterized programs such that the reduction R of a parameterized program P is again a parameterized program (the thread template of R is obtained by source-to-source transformation of the thread template of P). Consequently, existing techniques for the verification of parameterized programs can be directly applied to R instead of P. Our second technical contribution is that we define an appropriate family of pairwise preference orders which can be effectively used as a parameter to produce different lexicographical reductions. To determine whether this theoretical foundation amounts to a usable solution in practice, we have implemented the approach, based on a recently proposed framework for parameterized program verification. The results of our preliminary experiments on a representative set of examples are encouraging.

  @article{popl24:parameterizedCommutativity,
    author    = {Azadeh Farzan and Dominik Klumpp and Andreas Podelski},
    title     = {Commutativity Simplifies Proofs of Parameterized Programs},
    journal   = {Proc. {ACM} Program. Lang.},
    volume    = {8},
    number    = {{POPL}},
    year      = {2024},
    doi       = {10.1145/3632925}
  }

• Petrification: Software Model Checking for Programs with Dynamic Thread Management VMCAI'24
  

  Authors: Matthias Heizmann, Dominik Klumpp, Lars Nitzke, Frank Schüssele

  Springer Extended Version (arXiv) Recording

  We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present a reduction to the verification problem for concurrent programs with a fixed number of threads. More precisely, we present petrification, a transformation from programs with dynamic thread management to an existing, Petri net-based formalism for programs with a fixed number of threads. Our approach is implemented in a software model checking tool for C programs that use the pthreads API.

  @inproceedings{vmcai24:petrification,
    author       = {Matthias Heizmann and Dominik Klumpp and Lars Nitzke and Frank Sch{\"{u}}ssele},
    title        = {Petrification: Software Model Checking for Programs with Dynamic Thread Management},
    booktitle    = {{VMCAI} {(2)}},
    series       = {Lecture Notes in Computer Science},
    volume       = {14500},
    pages        = {3--25},
    publisher    = {Springer},
    year         = {2024},
    doi          = {10.1007/978-3-031-50521-8\_1}
  }

• Ultimate Taipan and Race Detection in Ultimate SV-COMP@ETAPS'23
  

  Authors: Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Frank Schüssele, Andreas Podelski

  Springer Artifact

  Ultimate Taipan integrates trace abstraction with algebraic program analysis on path programs. Taipan supports data race checking in concurrent programs through a reduction to reachability checking. Though the subsequent verification is not tuned for data race checking, the results are encouraging.

  @inproceedings{tacas23:ultimateTaipan,
    author    = {Daniel Dietsch and Matthias Heizmann and Dominik Klumpp and Frank Sch{\"{u}}ssele and Andreas Podelski},
    title     = {Ultimate Taipan and Race Detection in Ultimate (Competition Contribution)},
    booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
                 - 29th International Conference, {TACAS} 2023, Held as Part of the
                 European Joint Conferences on Theory and Practice of Software, {ETAPS}
                 2023, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
    publisher = {Springer},
    year      = {2023},
    doi       = {10.1007/978-3-031-30820-8\_40}
  }

• Ultimate Automizer and the CommuHash Normal Form SV-COMP@ETAPS'23
  

  Authors: Matthias Heizmann, Max Barth, Daniel Dietsch, Leonard Fichtner, Jochen Hoenicke, Dominik Klumpp, Mehdi Naouar, Tanja Schindler, Frank Schüssele, Andreas Podelski

  Springer Artifact

  The verification approach of Ultimate Automizer utilizes SMT formulas. This paper presents techniques to keep the size of the formulas small. We focus especially on a normal form, called CommuHash normal form that was easy to implement and had a significant impact on the runtime of our tool.

  @inproceedings{tacas23:ultimateAutomizer,
    author    = {Matthias Heizmann and Max Barth and Daniel Dietsch and Leonard Fichtner and Jochen Hoenicke and Dominik Klumpp and Mehdi Naouar and Tanja Schindler and Frank Sch{\"{u}}ssele and Andreas Podelski},
    title     = {Ultimate Automizer and the CommuHash Normal Form (Competition Contribution)},
    booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
                 - 29th International Conference, {TACAS} 2023, Held as Part of the
                 European Joint Conferences on Theory and Practice of Software, {ETAPS}
                 2023, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
    publisher = {Springer},
    year      = {2023},
    doi       = {10.1007/978-3-031-30820-8\_39}
  }

• Stratified Commutativity in Verification Algorithms for Concurrent Programs POPL'23
  

  Authors: Azadeh Farzan, Dominik Klumpp, Andreas Podelski

  ACM Slides Recording

  The importance of exploiting commutativity relations in verification algorithms for concurrent programs is well-known. They can help simplify the proof and improve the time and space efficiency. This paper studies commutativity relations as a first-class object in the setting of verification algorithms for concurrent programs. A first contribution is a general framework for abstract commutativity relations. We introduce a general soundness condition for commutativity relations, and present a method to automatically derive sound abstract commutativity relations from a given proof. The method can be used in a verification algorithm based on abstraction refinement to compute a new commutativity relation in each iteration of the abstraction refinement loop. A second result is a general proof rule that allows one to combine multiple commutativity relations, with incomparable power, in a stratified way that preserves soundness and allows one to profit from the full power of the combined relations. We present an algorithm for the stratified proof rule that performs an optimal combination (in a sense made formal), enabling usage of stratified commutativity in algorithmic verification. We empirically evaluate the impact of abstract commutativity and stratified combination of commutativity relations on verification algorithms for concurrent programs.

  @article{popl23:stratifiedCommutativity,
    author    = {Azadeh Farzan and Dominik Klumpp and Andreas Podelski},
    title     = {Stratified Commutativity in Verification Algorithms for Concurrent Programs},
    journal   = {Proc. {ACM} Program. Lang.},
    volume    = {7},
    number    = {{POPL}},
    pages     = {1426--1453},
    year      = {2023},
    doi       = {10.1145/3571242}
  }

• Sound Sequentialization for Concurrent Program Verification PLDI'22
  

  Authors: Azadeh Farzan, Dominik Klumpp, Andreas Podelski

  ACM Slides Recording Artifact

  We present a systematic investigation and experimental evaluation of a large space of algorithms for the verification of concurrent programs. The algorithms are based on sequentialization. In the analysis of concurrent programs, the general idea of sequentialization is to select a subset of interleavings, represent this subset as a sequential program, and apply a generic analysis for sequential programs. For the purpose of verification, the sequentialization has to be sound (meaning that the proof for the sequential program entails the correctness of the concurrent program). We use the concept of a preference order to define which interleavings the sequentialization is to select (“the most preferred ones”). A verification algorithm based on sound sequentialization that is parametrized in a preference order allows us to directly evaluate the impact of the selection of the subset of interleavings on the performance of the algorithm. Our experiments indicate the practical potential of sound sequentialization for concurrent program verification.

  @inproceedings{pldi22:soundSequentialization,
    author    = {Azadeh Farzan and Dominik Klumpp and Andreas Podelski},
    editor    = {Ranjit Jhala and Isil Dillig},
    title     = {Sound Sequentialization for Concurrent Program Verification},
    booktitle = {{PLDI} '22: 43rd {ACM} {SIGPLAN} International Conference on Programming
                 Language Design and Implementation, San Diego, CA, USA, June 13 -
                 17, 2022},
    pages     = {506--521},
    publisher = {{ACM}},
    year      = {2022},
    doi       = {10.1145/3519939.3523727}
  }

• Ultimate GemCutter and the Axes of Generalization SV-COMP@ETAPS'22
  

  Authors: Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, Andreas Podelski

  Springer Slides Artifact

  Ultimate GemCutter verifies concurrent programs using the CEGAR paradigm, by generalizing from spurious counterexample traces to larger sets of correct traces. We integrate classical CEGAR generalization with orthogonal generalization across interleavings. Thereby, we are able to prove correctness of programs otherwise out-of-reach for interpolation-based verification. The competition results show significant advantages over other concurrency approaches in the Ultimate family.

  @inproceedings{tacas22:ultimateGemCutter,
    author    = {Dominik Klumpp and Daniel Dietsch and Matthias Heizmann and Frank Sch{\"{u}}ssele and Marcel Ebbinghaus and Azadeh Farzan and Andreas Podelski},
    editor    = {Dana Fisman and Grigore Rosu},
    title     = {Ultimate GemCutter and the Axes of Generalization (Competition Contribution)},
    booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
                 - 28th International Conference, {TACAS} 2022, Held as Part of the
                 European Joint Conferences on Theory and Practice of Software, {ETAPS}
                 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part {II}},
    series    = {Lecture Notes in Computer Science},
    volume    = {13244},
    pages     = {479--483},
    publisher = {Springer},
    year      = {2022},
    doi       = {10.1007/978-3-030-99527-0\_35}
  }

• 𝕂 and KIV: Towards Deductive Verification for Arbitrary Programming Languages WADT@ETAPS'20
  

  Authors: Dominik Klumpp, Philip Lenzen

  Springer Slides Poster

  Deductive program verification is a powerful tool to gain confidence in the correctness of software. However, its application to real programs faces a major hurdle: Each programming language requires development of dedicated verification tool support. In this work, we aim to advance deductive software verification to arbitrary programming languages. We developed a tool that derives algebraic specifications for the deductive proof assistant KIV from the syntax and operational semantics of a programming language specified in the 𝕂 semantic framework. We adapt and implement the generic One-Path Reachability calculus and provide instant tool support for deductive proofs. Through a sophisticated automation approach, we drastically reduce the manual proof steps.

  @inproceedings{wadt20:KandKIV,
    author    = {Dominik Klumpp and Philip Lenzen},
    editor    = {Markus Roggenbach},
    title     = {{$\mathbb{K}$} and {KIV}:
                 Towards Deductive Verification for Arbitrary Programming Languages},
    booktitle = {Recent Trends in Algebraic Development Techniques - 25th International Workshop,
                 {WADT} 2020, Virtual Event, April 29, 2020, Revised Selected Papers},
    series    = {Lecture Notes in Computer Science},
    volume    = {12669},
    pages     = {98--119},
    publisher = {Springer},
    year      = {2020},
    doi       = {10.1007/978-3-030-73785-6\_6}
  }

• Verification of Concurrent Programs Using Petri Net Unfoldings VMCAI'21
  

  Authors: Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, Claus Schätzle

  Springer Slides Recording

  Given a verification problem for a concurrent program (with a fixed number of threads) over infinite data domains, we can construct a model checking problem for an abstraction of the concurrent program through a Petri net (a problem which can be solved using McMillan’s unfoldings technique). We present a method of abstraction refinement which translates Floyd/Hoare-style proofs for sample traces into additional synchronization constraints for the Petri net.

  @inproceedings{vmcai21:petriNetUnfoldings,
    author    = {Daniel Dietsch and Matthias Heizmann and Dominik Klumpp and Mehdi Naouar and Andreas Podelski and Claus Sch{\"{a}}tzle},
    editor    = {Fritz Henglein and Sharon Shoham and Yakir Vizel},
    title     = {Verification of Concurrent Programs Using Petri Net Unfoldings},
    booktitle = {Verification, Model Checking, and Abstract Interpretation - 22nd International
                 Conference, {VMCAI} 2021, Copenhagen, Denmark, January 17-19, 2021,
                 Proceedings},
    series    = {Lecture Notes in Computer Science},
    volume    = {12597},
    pages     = {174--195},
    publisher = {Springer},
    year      = {2021},
    doi       = {10.1007/978-3-030-67067-2\_9}
  }

• Partial Order Reduction for Trace Abstraction Refinement MOVEP'20
  

  Authors: Dominik Klumpp

  MOVEP Slides Recording

  It is well-known that concurrent programs suffer from the state explosion problem: Due to the non-deterministic scheduling of different threads, the number of reachable program states grows exponentially in the number of threads. Accordingly, the runtime of static analyses or verification algorithms also grows exponentially in the number of threads. In this research, we focus on improving the efficiency of Trace Abstraction Refinement (TAR), a Software Model Checking technique, when applied to concurrent programs. We achieve this by integrating it with Partial Order Reduction (POR), a technique from the field of (finite-state) model checking that combats the state explosion problem. This work is done in collaboration with Azadeh Farzan and Andreas Podelski.

  @inproceedings{movep20:POR4TAR,
    author       = {Dominik Klumpp},
    title        = {Partial Order Reduction for Trace Abstraction Refinement},
    booktitle    = {14th Summer School on Modelling and Verification of Parallel Processes, {MOVEP} 2020, June 22-26, 2020}
    howpublished = {\url{http://projects-verimag.imag.fr/movep2020/student-talks/}},
    year         = {2020}
  }

• Automated Control Flow Reconstruction from Assembler Programs (MSc thesis)

  Authors: Dominik Klumpp

  University of Augsburg Slides

  As software permeates more and more aspects of daily life and becomes a central component of critical systems around the world, software quality and effective methods to ensure it are paramount. There is a huge variety of both static and dynamic analyses that aim to provide such guarantees. Typically, such analyses are based on the analysed program’s control flow graph (CFG). Given the source code of the program in a high-level, structured programming language, this graph can easily be constructed. However, in some cases the analysis must instead be based directly on the binary program, e.g. if the source code is not available (in security contexts), contains insufficient information (e.g. for low-level analyses such as execution time) or the compiler is not trusted to translate the source code faithfully to a binary format. However, extracting the control flow graph from a binary program is a non-trivial task, as the binary code is unstructured and contains indirect branches that transfer control to a program location dynamically computed at runtime. This thesis defines a formal notion of a CFG for a binary program and proposes several quality requirements such CFGs should meet in order to be considered a sufficiently precise approximation of the program. A more precise CFG improves the efficiency and potentially the accuracy of subsequent analyses. In particular, we define the property of being free from control flow errors and postulate that precise CFGs should satisfy this property. The CFGs produced by existing approaches to control flow reconstruction from binary programs do not meet all of these requirements. A new approach to control flow reconstruction is thus presented, based on the formal verification technique trace abstraction refinement. This verification technique is adapted to the field of control flow reconstruction, and the computed CFGs are shown to be sound over-approximations of the program behaviour. A sufficient condition is presented under which the CFGs are furthermore free from control flow errors. We evaluate the new approach empirically on a set of standard benchmark programs.

  @thesis{mscthesis:automatedCFGReconstruction,
    type    = {Master's thesis},
    author  = {Dominik Klumpp},
    title   = {Automated Control Flow Reconstruction from Assembler Programs},
    school  = {University of Augsburg},
    year    = {2018},
    month   = dec,
    address = {Augsburg, Germany},
    doi     = {10.13140/RG.2.2.27544.65283}
  }

• Measuring and Evaluating the Performance of Self-Organization Mechanisms Within Collective Adaptive Systems ISoLA'18
  

  Authors: Benedikt Eberhardinger, Hella Ponsar, Dominik Klumpp, Wolfgang Reif

  Springer

  By restructuring and reconfiguring itself at run-time, a collective adaptive system (CAS) is able to fulfill its requirements under uncertain, ever-changing environmental conditions. Indeed, this process of self-organization (SO) is of utmost importance for the ability of the CAS to perform. However, it is hard to design high-performing SO mechanisms, because the environmental conditions are partially unpredictable at design time. Thus, a crucial aid for the development of SO mechanisms is a tool set enabling performance evaluations at design time in order to select the best-fitting mechanism and parametrize it. We present a metric for measuring the performance of an SO mechanism as well as a framework that enables evaluation of this metric. The proposed metric is evaluated for different kinds of SO mechanisms in two case studies: a smart energy management system and a self-organizing production cell.

  @inproceedings{isola18:measureSO,
    author    = {Benedikt Eberhardinger and Hella Ponsar and Dominik Klumpp and Wolfgang Reif},
    editor    = {Tiziana Margaria and Bernhard Steffen},
    title     = {Measuring and Evaluating the Performance of Self-Organization Mechanisms Within Collective Adaptive Systems},
    booktitle = {Leveraging Applications of Formal Methods, Verification and Validation. 
                 Distributed Systems - 8th International Symposium, ISoLA 2018, Limassol,
                 Cyprus, November 5-9, 2018, Proceedings, Part {III}},
    series    = {Lecture Notes in Computer Science},
    volume    = {11246},
    pages     = {202--220},
    publisher = {Springer},
    year      = {2018},
    doi       = {10.1007/978-3-030-03424-5\_14}
  }

• Test Case Selection Strategy for Self-Organization Mechanisms

  Authors: Benedikt Eberhardinger, Hella Ponsar, Dominik Klumpp, Wolfgang Reif

  dpunkt.verlag

  A major challenge of testing self-organization mechanisms is to cover the large state space that is due to the autonomy of the system and the partially unpredictable environment it has to operate in. This challenges the test case generation and selection, since exhaustive testing is largely impossible and the adequacy of a test suite depends on run-time aspects, e.g., the current structure of the system in its environment. We present an approach for test case generation and selection, which is tailored for self-organization mechanisms and their characteristics. Thus, it is possible to efficiently reduce the number of test cases compared to a random selection strategy by not losing adequacy. We show this in an empirical evaluation of a self-organizing production cell scenario.

  @inbook{tav17:testCaseSelection4SO,
    author    = {Benedikt Eberhardinger and Hella Ponsar and Dominik Klumpp and Wolfgang Reif},
    editor    = {Andreas Spillner and Mario Winter and Andrej Pietschker},
    title     = {Test Case Selection Strategy for Self-Organization Mechanisms},
    booktitle = {Test, Analyse und Verifikation von Software -- gestern, heute, morgen},
    pages     = {139--156},
    publisher = {dpunkt.verlag},
    year      = {2017}
  }

• Optimising Runtime Safety Analysis Efficiency for Self-Organising Systems QA4SASO@SASO'16
  

  Authors: Dominik Klumpp, Axel Habermaier, Benedikt Eberhardinger, Hella Ponsar

  IEEE

  Self-organising resource-flow systems typically have a high tolerance for component faults: When a component fails, the system can use another component of the same type instead. However, this redundancy is eventually exhausted: If enough components fail, they can no longer be replaced and the system ceases to function. An analysis of these self-organisation limits is essential to assess the system’s safety but difficult to perform at design time because the system’s structure and behaviour are hard to predict. By contrast, runtime analyses are subject to high performance demands. This paper presents several techniques that significantly reduce analysis time in order to facilitate safety analyses at runtime. We model a self-organising system producing personalised medicine and use it to evaluate these techniques.

  @inproceedings{qa4saso16:optimisingSafety,
    author    = {Dominik Klumpp and Axel Habermaier and Benedikt Eberhardinger and Hella Seebach},
    editor    = {Sameh Elnikety and Peter R. Lewis and Christian M{\"{u}}ller{-}Schloer},
    title     = {Optimising Runtime Safety Analysis Efficiency for Self-Organising Systems},
    booktitle = {2016 {IEEE} 1st International Workshops on Foundations and Applications
                 of Self* Systems (FAS*W), Augsburg, Germany, September 12-16, 2016},
    pages     = {120--125},
    publisher = {{IEEE}},
    year      = {2016},
    doi       = {10.1109/FAS-W.2016.37}
  }

• Optimising Runtime Safety Analysis Efficiency for Self-Organising Systems (BSc thesis)

  Authors: Dominik Klumpp

  University of Augsburg

  One key advantage of many self-organising resource-flow systems is their high tolerance for component faults: The system can compensate for the failure of a component by using another component of the same type instead. However, if enough components fail, this redundancy is eventually exhausted: Failed components can no longer be replaced and the system ceases to function. An analysis of these fault tolerance limits is essential to assess the system’s safety. Furthermore, analyses at runtime can be used to predict and possibly prevent system failures and thus increase the system’s safety. Unfortunately, conducting these analyses proves difficult: At design time, the system’s runtime behaviour is hard to predict. Runtime analyses on the other hand are subject to high performance demands. This thesis presents several optimisation techniques for such analyses in order to facilitate analyses at runtime. A self-organising system producing personalised medicine is modeled and used to evaluate these optimisation techniques.

  @thesis{bsc:optimiseSafety4SOS,
    type    = {Bachelor's thesis},
    author  = {Dominik Klumpp},
    title   = {Optimising Runtime Safety Analysis Efficiency for Self-Organising Systems},
    school  = {University of Augsburg},
    year    = {2016},
    month   = sep,
    address = {Augsburg, Germany}
  }