Logo des Repositoriums

Auflistung nach Autor:in "Jakobs, Marie-Christine"

1 - 6 von 6
  • 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
    Cooperative Test-Case Generation with Verifiers
    (Software Engineering 2020, 2020) Beyer, Dirk; Jakobs, Marie-Christine
    Software testing is widely applied in software quality assurance. Often, test suites fulfilling a certain coverage measure must be constructed. Manually constructing them is laborious. However, numerous automatic test-generation approaches exist. Due to various strengths and weaknesses of individual approaches, hybrid approaches, which combine different approaches, construct test suites that achieve higher coverage values than test suites generated by individual approaches. We propose the hybrid test-generation approach CoVeriTest. CoVeriTest is flexible, cooperative, and based on verification technology. It iteratively executes a sequence of verifiers that may exchange analysis information between each other and output a test case whenever they reach a test goal. The verifiers, their individual time limits, and which analysis information is exchanged between them is configurable. We experimented with different CoVeriTest configurations. The best configuration participated in the 1st International Competition on Software Testing (Test-Comp’19) and won the third place. This proves the value of our CoVeriTest approach.
  • Konferenzbeitrag
    Just test what you cannot verify!
    (Software Engineering 2016, 2016) Czech, Mike; Jakobs, Marie-Christine; Wehrheim, Heike
    Software verification is an established method to ensure software safety. Nevertheless, verification still often fails, either because it consumes too much resources, e.g., time or memory, or the technique is not mature enough to verify the property. Often then discarding the partial verification, the validation process proceeds with techniques like testing. To enable standard testing to profit from previous, partial verification, we use a summary of the verification effort to simplify the program for subsequent testing. Our techniques use this summary to construct a residual program which only contains program paths with unproven assertions. Afterwards, the residual program can be used with standard testing tools. Our first experiments show that testing profits from the partial verification. The test effort is reduced and combined verification and testing is faster than a complete verification.
  • Konferenzbeitrag
    On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring
    (Ausgezeichnete Informatikdissertationen 2017, 2018) Jakobs, Marie-Christine
  • 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.