Logo des Repositoriums

Auflistung nach Autor:in "Haltermann, Jan"

1 - 4 von 4
  • Konferenzbeitrag
    Component-based CEGAR - Building Software Verifiers from Off-the-Shelf Components
    (Software Engineering 2023, 2023) Beyer, Dirk; Haltermann, Jan; Lemberger, Thomas; Wehrheim, Heike
    Software verification tools typically consist of tighly coupled components, thereby precluding the easy integration of off-the-shelf components. We propose to decompose software verification into independent subtasks, each task being implemented by an own component communicating with other components via clearly defined interfaces. We apply this idea of decomposition to one of the most frequently used techniques in software verification: CEGAR. Our decomposition, called component-based CEGAR (C-CEGAR), comprises three components: An abstract model explorer, a feasibility checker and a precision refiner. It allows employing conceptually different components for each task within one instance. Our evaluation shows that C-CEGAR has, compared to a monolithic CEGAR-implementation, a similar efficiency and that the precision in solving verification tasks even increases.
  • Konferenzbeitrag
    CoVEGI: Cooperative Verification via Externally Generated Invariants
    (Software Engineering 2022, 2022) Haltermann, Jan; Wehrheim, Heike
    Software verification has recently made enormous progress. To keep their tools up to date with novel methods and enhanced techniques, tool developers integrate these within their own framework almost exclusively by re-implementation. While this allows for a conceptual re-use of methods, it nevertheless requires novel implementations. Our configurable framework named CoVEGI employs cooperative verification in order to avoid re-implementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for invariant generation, which is key to the success of a verification run. CoVEGI allows a main verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators, utilizing their results within its verification run. The experimental evaluation shows that the use of CoVEGI can increase the number of correctly verified tasks up to 17%, without increasing the used resources.
  • Konferenzbeitrag
    Ranged Program Analysis: A Parallel Divide-and-Conquer Approach for Software Verification
    (Software Engineering 2024 (SE 2024), 2024) Haltermann, Jan; Jakobs, Marie-Christine; Richter, Cedric; Wehrheim, Heike
  • Konferenzbeitrag
    Variable Misuse Detection: Software Developers versus Neural Bug Detectors
    (Software Engineering 2023, 2023) Richter, Cedric; Haltermann, Jan; Jakobs, Marie-Christine; Pauck, Felix; Schott, Stefan; Wehrheim, Heike
    Finding and fixing software bugs is a central part of software development. Developers are therefore often confronted with the task of identifying whether a code snippet contains a bug and where it is located. Recently, data-driven approaches have been employed to automate this process. These so called neural bug detectors are trained on millions of buggy and correct code snippets to learn the task of bug detection. This raises the question how the performance of neural bug detectors and software developers compare. As a first step, we study this question in the context of variable misuse bugs. To this end, we performed a study with over 100 software developers and two state-of-the-art approaches for neural bug detection. Our study shows that software developers are on average slightly better than neural bug detectors – even though the bug detectors are trained specifically for this task. In addition, we identified several bottlenecks in existing neural bug detectors which could be mitigated in the future to improve their bug detection performance.