Logo des Repositoriums

Auflistung nach Schlagwort "Software Verification"

1 - 5 von 5
  • 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
    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
    Data-Driven Design and Evaluation of SMT Meta-Solving Strategies
    (Software Engineering 2022, 2022) Mues, Malte; Howar, Falk
    The 36th IEEE/ACM International Conference on Automated Software Engineering (2021) accepted the paper ‘Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost’ [MH21a] and selected it for an ACM SIGSOFT Distinguished Paper Award. The paper presents four generally applicable patterns for the combination of multiple SMT decision procedures in a meta-solving strategy and demonstrates how a meta-solving strategy for string constraints can be developed in a data-driven approach based on these patterns: The paper cleans up and merges existing collections of SMT benchmarks in string theory solving to evaluate and compare derived meta-solving strategies. Notably, we can demonstrate on the available data that commonly used strategies as earliest returning SMT solver do not always return the most reliable result if all available SMT solvers are combined. Instead, cross-checking strategies work slightly better at moderate overhead.
  • Textdokument
    Model-in-the-Loop and Software-in-the-Loop Testing of Closed-Loop Automotive Software with Arttest
    (INFORMATIK 2017, 2017) Hansen, Norman; Wiechowski, Norbert; Kugler, Alexander; Kowalewski, Stefan; Rambow, Thomas; Busch, Rainer
    In this paper, we present Arttest, a tool for functional testing of block diagrams developed with MATLAB/Simulink. We introduce testing concepts for closed-loop tests of automotive software on model and software level, the integration of the concepts into a signal specification language and correspondent tool support. Furthermore, we show the applicability of the concepts and the test execution automation based on an example for model-in-the-loop and software-in-the-loop tests.
  • 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