Publications

full bibliography (BibTeX)

• Effective AGM Belief Contraction: A Journey beyond the Finitary Realm KR'25
  

  Authors: Dominik Klumpp, Jandson S. Ribeiro

  (to appear) Extended Version (arXiv)

  Despite significant efforts towards extending the AGM paradigm of belief change beyond finitary logics, the computational aspects of AGM have remained almost untouched. We investigate the computability of AGM contraction on non-finitary logics, and show an intriguing negative result: there are infinitely many uncomputable AGM contraction functions in such logics. Drastically, we also show that the current de facto standard strategies to control computability, which rely on restricting the space of epistemic states, fail: uncomputability remains in all non-finitary cases. Motivated by this disruptive result, we propose new approaches to controlling computability beyond the finitary realm. Using Linear Temporal Logic (LTL) as a case study, we identify an infinite class of fully-rational AGM contraction functions that are computable by design. We use Büchi automata to construct such functions, and to represent and reason about LTL beliefs.

  @inproceedings{kr25:effectiveAGMContraction,
    author       = {Dominik Klumpp and Jandson S. Ribeiro},
    editor       = {Renata Wassermann and Torsten Schaub},
    title        = {Effective {AGM} Belief Contraction:
                    A Journey beyond the Finitary Realm},
    booktitle    = {Proceedings of the 22nd International Conference on Principles of
                    Knowledge Representation and Reasoning, {KR} 2025, Melbourne, Australia.
                    November 11-17, 2025},
    year         = {2025},
    doi          = {---},
    note         = {(to appear)}
  }

• Counterexample-Guided Commutativity CAV'25
  

  Authors: Marcel Ebbinghaus, Dominik Klumpp, Andreas Podelski

  Springer Artifact

  We consider the use of commutativity-based reduction for the algorithmic verification of concurrent programs. In existing work, the commutativity relation used for the reduction is mostly fixed statically. In this paper, we propose a demand-driven approach to compute the commutativity relation. The approach can be viewed as the direct analogue of the CEGAR approach which uses counterexamples to guide the incremental refinement of the abstraction. Instead of eliminating a counterexample by proving it infeasible and refining the abstraction, we can eliminate a counterexample by proving it redundant and expanding the commutativity relation. When we prove a counterexample redundant, we use the proof for a generalization step which allows us to eliminate not just a single counterexample, but a whole infinite set. We present a general scheme where we integrate the new approach with the CEGAR approach. We have implemented an instantiation of the general scheme. An experimental evaluation shows an increase in the number of successfully verified programs by 15% on a challenging benchmark set.

  @article{cav25:counterexampleGuidedCommutativity,
    author       = {Marcel Ebbinghaus and Dominik Klumpp and Andreas Podelski},
    editor       = {Ruzica Piskac and Zvonimir Rakamaric},
    title        = {Counterexample-Guided Commutativity},
    booktitle    = {Computer Aided Verification - 37th International Conference, {CAV}
                    2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part {III}},
    series       = {Lecture Notes in Computer Science},
    volume       = {15933},
    pages        = {347--369},
    publisher    = {Springer},
    year         = {2025},
    doi          = {10.1007/978-3-031-98682-6\_18},
  }

• Correctness Witnesses with Function Contracts

  Authors: Matthias Heizmann, Dominik Klumpp, Marian Lingsch-Rosenfeld, Frank Schüssele

  Preprint (arxiv)

  Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing other tools to reproduce the verification results. Correctness witnesses in the current format (version 2.0) allow only for the encoding of loop and location invariants using C expressions. This limits the correctness arguments that verifiers can express in the witness format. One particular limitation is the inability to express function contracts, which consist of a pre-condition and a post-condition for a function. We propose an extension to the existing witness format 2.0 to allow for the specification of function contracts. Our extension includes support for several features inspired by ACSL (\result, \old, \at). This allows for the export of more information from tools and for the exchange of information with tools that require function contracts.

  @article{arxiv25:contractWitnesses,
    author       = {Matthias Heizmann and Dominik Klumpp and Marian Lingsch-Rosenfeld and Frank Sch\"ussele},
    title        = {Correctness Witnesses with Function Contracts},
    journal      = {CoRR},
    volume       = {abs/2501.12313},
    year         = {2025},
    doi          = {10.48550/arXiv.2501.12313}
  }

• Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts VMCAI'25
  

  Authors: Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schüssele, Michael Schwarz, Helmut Seidl, Sarah Tilscher, Vesal Vojdani

  Springer Extended Version (arXiv) Artifact

  Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists – in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75% of these witnesses – indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches.

  @inproceedings{vmcai25:ghost-witnesses,
    author       = {Julian Erhard and Manuel Bentele and Matthias Heizmann and Dominik Klumpp
                    and Simmo Saan and Frank Sch{\"{u}}ssele and Michael Schwarz and Helmut Seidl
                    and Sarah Tilscher and Vesal Vojdani},
    title        = {Correctness Witnesses for Concurrent Programs:
                    Bridging the Semantic Divide with Ghosts},
    booktitle    = {{VMCAI} {(1)}},
    series       = {Lecture Notes in Computer Science},
    volume       = {15529},
    pages        = {74--100},
    publisher    = {Springer},
    year         = {2025},
    doi          = {10.1007/978-3-031-82700-6\_4}
  }

• Walking the Tightrope between Expressiveness and Uncomputability: AGM Contraction beyond the Finitary Realm NMR@KR'24
  

  Authors: Dominik Klumpp, Jandson S. Ribeiro

  CEUR Extended Version

  Although there has been significant interest in extending the AGM paradigm of belief change beyond finitary logics, the computational aspects of AGM have remained almost untouched. We investigate the computability of AGM contraction on non-finitary logics, and show an intriguing negative result: there are infinitely many uncomputable AGM contraction functions in such logics. Drastically, even if we restrict the theories used to represent epistemic states, in all non-trivial cases, the uncomputability remains. On the positive side, we use Büchi automata to construct computable AGM contraction functions on Linear Temporal Logic (LTL).

  @inproceedings{nmr24:AGMBeyondFinitary,
    author       = {Dominik Klumpp and Jandson S. Ribeiro},
    editor       = {Nina Gierasimczuk and Jesse Heyninck},
    title        = {Walking the Tightrope between Expressiveness and Uncomputability:
                    {AGM} Contraction beyond the Finitary Realm},
    booktitle    = {Proceedings of the 22nd International Workshop on Nonmonotonic Reasoning
                    {(NMR} 2024) co-located with 21st International Conference on Principles
                    of Knowledge Representation and Reasoning {(KR} 2024), Hanoi, Vietnam,
                    November 2-4, 2024},
    series       = {{CEUR} Workshop Proceedings},
    volume       = {3835},
    pages        = {34--43},
    publisher    = {CEUR-WS.org},
    year         = {2024},
    url          = {https://ceur-ws.org/Vol-3835/paper4.pdf}
  }

• 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}},
    pages     = {2485--2513},
    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}
  }