16 citations · 43 across the 11 of their papers we have counts for
11 papers
Feedback Loops and Code Perturbations in LLM-based Software Engineering: A Case Study on a C-to-Rust Translation System
Martin Weiss, Jesko Hecking-Harbusch, Jochen Quante +1
The advent of strong generative AI has a considerable impact on various software engineering tasks such as code repair, test generation, or language translation. While tools like G…
Formal Runtime Error Detection During Development in the Automotive Industry
Jesko Hecking-Harbusch, Jochen Quante, Maximilian Schlund
Modern automotive software is highly complex and consists of millions lines of code. For safety-relevant automotive software, it is recommended to use sound static program analysis…
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specificatio…
A Web Interface for Petri Nets with Transits and Petri Games
Manuel Gieseking, Jesko Hecking-Harbusch, Ann Yanich
Developing algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms…
Model Checking Branching Properties on Petri Nets with Transits (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
To model check concurrent systems, it is convenient to distinguish between the data flow and the control. Correctness is specified on the level of data flow whereas the system is c…
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more con…
Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems
Jesko Hecking-Harbusch, Niklas O. Metzger
The manual implementation of distributed systems is an error-prone task because of the asynchronous interplay of components and the environment. Bounded synthesis automatically gen…
Model Checking Data Flows in Concurrent Network Updates (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
We present a model checking approach for the verification of data flow correctness in networks during concurrent updates of the network configuration. This verification problem is…
Translating Asynchronous Games for Distributed Synthesis (Full Version)
Raven Beutner, Bernd Finkbeiner, Jesko Hecking-Harbusch
In distributed synthesis, we generate a set of process implementations that, together, accomplish an objective against all possible behaviors of the environment. A lot of recent wo…
Symbolic vs. Bounded Synthesis for Petri Games
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
Petri games are a multiplayer game model for the automatic synthesis of distributed systems. We compare two fundamentally different approaches for solving Petri games. The symbolic…
Solving QBF by Abstraction
Jesko Hecking-Harbusch, Leander Tentrup
Many verification and synthesis approaches rely on solving techniques for quantified Boolean formulas (QBF). Consequently, solution witnesses, in the form of Boolean functions, bec…