Logo des Repositoriums

Auflistung nach Autor:in "Lemberger, Thomas"

1 - 3 von 3
  • Konferenzbeitrag
    Combining Verifiers in Conditional Model Checking via Reducers
    (Software Engineering and Software Management 2019, 2019) Beyer, Dirk; Jakobs, Marie-Christine; Lemberger, Thomas; Wehrheim, Heike
    Software verification received lots of attention in the past two decades. Nonetheless, it remains an extremely difficult problem. Some verification tasks cannot be solved automatically by any of today’s verifiers. To still verify such tasks, one can combine the strengths of different verifiers. A promising approach to create combinations is conditional model checking (CMC). In CMC, the first verifier outputs a condition that describes the parts of the program state space that it successfully verified, and the next verifier uses that condition to steer its exploration towards the unverified state space. Despite the benefits of CMC, only few verifiers can handle conditions. To overcome this problem, we propose an automatic plug-and-play extension for verifiers. Instead of modifying verifiers, we suggest to add a preprocessor: the reducer. The reducer takes the condition and the original program and computes a residual program that encodes the unverified state space in program code. We developed one such reducer and use it to integrate existing verifiers and test-case generators into the CMC process. Our experiments show that we can solve many additional verification tasks with this reducer-based construction.
  • 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.
  • Zeitschriftenartikel
    Cooperative Approaches Across Test Generation and Formal Software Verification
    (Softwaretechnik-Trends Band 44, Heft 2, 2024) Lemberger, Thomas
    In the last decade, powerful techniques were developed that either automatically generate tests for software, or automatically verify software with formal methods. In both areas it is common to combine different techniques to leverage their strengths and mitigate their weaknesses. This happens through costly, proprietary reimplementations within a single tool. This thesis contrasts this and provide concepts that enable an inexpensive and fast off-the-shelf cooperation of standalone tools through standardized exchange formats.