Logo des Repositoriums

Auflistung nach Autor:in "Beyer, Dirk"

1 - 10 von 10
  • 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.
  • 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
    Exchanging Verification Witnesses between Verifiers
    (Software Engineering 2017, 2017) Beyer, Dirk; Dangl, Matthias; Dietsch, Daniel; Heizmann, Matthias
    Standard verification tools provide a counterexample to witness a specifica- tion violation. Since a few years, such a witness can be validated by an independent validator using an exchangeable witness format. This way, information about the violation can be shared across verifiers and the user can use standard tools to visualize and explore witnesses. This technique is not yet established for the correctness case, where a program fulfills a specification. Even for simple programs, users often struggle to comprehend why a program is correct, and there is no way to independently check the verification result. We recently closed this gap by complementing our earlier work on violation witnesses with correctness witnesses. The overall goal to make proofs avail- able to engineers is probably as old as programming itself, and proof-carrying code was proposed two decades ago — our goal is to make it practical: We consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the principle of separation of concerns. At any time, the correctness witness can be used to recon- struct a correctness proof to establish trust. We extended two state-of-the-art verifiers, CPACHECKER and ULTIMATEAUTOMIZER, to produce and validate witnesses.
  • Konferenzbeitrag
    Interpolation for value analysis
    (Software-engineering and management 2015, 2015) Beyer, Dirk; Löwe, Stefan
    Abstraction, counterexample-guided refinement, and interpolation are techniques that are essential to the success of predicate-based program analysis. These techniques have not yet been applied together to value analysis. We present an approach that integrates abstraction and interpolation-based refinement into a value analysis, i.e., a program analysis that tracks values for a specified set of variables (the precision).
  • Konferenzbeitrag
    On facilitating reuse in multi-goal test-suite generation for software product lines
    (Software Engineering 2016, 2016) Lochau, Malte; Bürdek, Johannes; Bauregger, Stefan; Holzer, Andreas; Rhein, Alexander Von; Apel, Sven; Beyer, Dirk
    Software testing is still the most established and scalable quality-assurance technique in practice today. However, generating effective test suites remains computationally expensive, consisting of repetitive reachability analyses for multiple test goals according to a coverage criterion. This situation is even worse when it comes to testing of entire software product lines (SPL). An SPL consists of a family of similar program variants, thus testing an SPL requires a sufficient coverage of all derivable program variants. Instead of considering every product variant one-by-one, family-based approaches are variability-aware analysis techniques in that they systematically explore similarities among the different variants. Based on this principle, we propose a novel approach for automated product-line test-suite generation incorporating extensive reuse of reachability information among test cases derived for different test goals and/or program variants. The developed tool implementation is built on top of CPA/TIGER which is based on CPACHECKER. We further present experimental evaluation results, revealing a considerable increase in efficiency compared to existing test-case generation techniques. Software product line (SPL) engineering aims at developing families of similar, yet welldistinguished software products built upon a common core platform. The commonality and variability among the family members (product variants) of an SPL are specified as features. In this regard, a feature corresponds to user-configurable product characteristics within the problem domain, as well as implementation artifacts being automatically composeable into implementation variants. The resulting extensive reuse of common feature artifacts among product variants facilitates development efficiency as well as product quality compared to one-by-one variant development. However, for SPLs to become fully accepted in practice, software-quality assurance techniques have to become variabilityaware, too, in order to benefit from SPL reuse principles. In practice, systematic software testing constitutes the most elaborated and wide-spread assurance technique, being directly applicable to software systems at any level of abstraction. In addition, testing enables a controllable trade-off between effectiveness and efficiency. In particular, white-box test generation consists of (automatically) deriving input vectors for a program under test with respect to predefined test goals. The derivation of sufficiently large test suites is, therefore, guided by test selection metrics, e.g., structural coverage criteria like basic block coverage and condition coverage [Be13]. These criteria impose multiple test goals, thus requiring sets of test input vectors for their complete coverage [Be13]. In case of mission-/safety- 1 This is a summary of a full article on this topic that appeared in Proc. FASE 2015 [Bü15]. 2 This work was partially supported by the DFG (German Research Foundation) under the Priority Programme SPP1593: Design For Future - Managed Software Evolution. 3 TU Darmstadt, Germany 4 TU Wien, Austria 5 University of Passau, Germany critical systems, it is imperative, or even enforced by industrial standards to guarantee a particular degree of code coverage for every delivered product. Technically, automated test input generation requires expensive reachability analyses of the program state space. Symbolic model checking is promising approach for fully automated white-box test generation using counterexamples as test inputs [Be04]. Nevertheless, concerning large sets of complex test goals, scalability issues still obstruct efficient test case generation when being performed for every test goal in separate. This problem becomes even worse while generating test inputs for covering entire product line implementations. To avoid a variantby-variant (re-)generation of test cases potentially leading to many redundant generation runs, an SPL test-suite generation approach must enhance existing techniques. In [Bü15], we presented a novel technique for efficient white-box test-suite generation for multi-goal test coverage of product-line implementations. The approach systematically exploits reuse potentials among reachability analysis results by means of similarity among test cases (1) derived for different test goals [Be13], and/or (2) derived for different product variants [Ci11]. The combination of both techniques allows for an incremental, coveragedriven exploration of the state space of entire product lines under test implemented in C enriched with feature parameters. We implemented an SPL test-suite generator for arbitrary coverage criteria on top of the symbolic software model checker CPACHECKER [Be13]. We evaluated our technique considering sample SPL implementations of varying size. Our experiments revealed the applicability of the tool to real-world SPL implementations, as well as a remarkable gain in efficiency obtained from the reuse of reachability analysis results. compared to test suite generation approaches without systematic reuse. As a future work, we plan to improve reuse capabilities by applying multi-property model-checking techniques of CPACHECKER which allows for reachability analyses of multiple test goals in a single run. Literaturverzeichnis [Be04] Beyer, Dirk; Chlipala, Adam J.; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: Generating Tests from Counterexamples. In: ICSE. pp. 326-335, 2004. [Be13] Beyer, Dirk; Holzer, Andreas; Tautschnig, Michael; Veith, Helmut: Information Reuse for Multi-goal Reachability Analyses. In: ESOP, pp. 472-491. Springer, 2013. [Bü15] Bürdek, Johannes; Lochau, Malte; Bauregger, Stefan; Holzer, Andreas; von Rhein, Alexander; Apel, Sven; Beyer, Dirk: Facilitating Reuse in Multi-Goal Test-Suite Generation for Software Product Lines. In: FASE. Springer, 2015. [Ci11] Cichos, Harald; Oster, Sebastian; Lochau, Malte; Schürr, Andy: Model-based Coverage- Driven Test Suite Generation for Software Product Lines. In: MoDELS. Springer, pp. 425-439, 2011.
  • Konferenzbeitrag
    Precision reuse in CPAchecker
    (Software Engineering 2014, 2014) Beyer, Dirk; Löwe, Stefan; Novikov, Evgeny; Stahlbauer, Andreas; Wendler, Philipp
  • Konferenzbeitrag
    A Retrospective Study of one Decade of Artifact Evaluations
    (Software Engineering 2024 (SE 2024), 2024) Winter, Stefan; Timperley, Christopher; Hermann, Ben; Cito, Jürgen; Bell, Jonathan; Hilton, Michael; Beyer, Dirk
  • Konferenzbeitrag
    Reusing information in multi-goal reachability analyses
    (Software Engineering 2014, 2014) Beyer, Dirk; Holzer, Andreas; Tautschnig, Michael; Veith, Helmut
  • Konferenzbeitrag
    Verification Witnesses
    (Software Engineering 2016, 2016) Beyer, Dirk; Dangl, Matthias; Dietsch, Daniel; Heizmann, Matthias; Stahlbauer, Andreas
    It is commonly understood that a verification tool should provide a counterex-ample to witness a specification violation. Until recently, software verifiers dumped error witnesses in proprietary formats, which are often neither humannor machine-readable, and an exchange of witnesses between different verifiers was impossible. We have defined an exchange format for error witnesses that is easy to write and read by verification tools (for further processing, e.g., witness validation). To eliminate manual inspection of false alarms, we develop the notion of stepwise testification: in a first step, a verifier finds a problematic program path and, in addition to the verification result FALSE, constructs a witness for this path; in the next step, another verifier re-verifies that the witness indeed violates the specification. This process can have more than two steps, each reducing the state space around the error path, making it easier to validate the witness in a later step. An obvious application for testification is the setting where we have two verifiers: one that is efficient but imprecise and another one that is precise but expensive. The technique of error-witness-driven program analysis is implemented in two state-of-the-art verification tools, CPACHECKER and ULTIMATE AUTOMIZER.