Logo des Repositoriums

Auflistung nach Autor:in "Wehrheim, Heike"

1 - 10 von 15
  • Zeitschriftenartikel
    A Case for a New IT Ecosystem: On-The-Fly Computing
    (Business & Information Systems Engineering: Vol. 62, No. 6, 2020) Karl, Holger; Kundisch, Dennis; Meyer auf der Heide, Friedhelm; Wehrheim, Heike
    The complexity of development and deployment in today’s IT world is enormous. Despite the existence of so many pre-fabricated components, frameworks, cloud providers, etc., building IT systems still remains a major challenge and most likely overtaxes even a single ambitious developer. This results in spreading such development and deployment tasks over different team members with their own specialization. Nevertheless, not even highly competent IT personnel can easily succeed in developing and deploying a nontrivial application that comprises a multitude of different components running on different platforms (from frontend to backend). Current industry trends such as DevOps strive to keep development and deployment tasks tightly integrated. This, however, only partially addresses the underlying complexity of either of these two tasks. But would it not be desirable to simplify these tasks in the first place, enabling one person – maybe even a non-expert – to deal with all of them? Today’s approaches to the development and deployment of complex IT applications are not up to this challenge. “On-The-Fly Computing” offers an approach to tackle this challenge by providing complex IT services through largely automated configuration and execution. The configuration of such services is based on simple, flexibly combinable services that are provided by different software providers and traded in a market. This constitutes a highly relevant challenge for research in many branches of computer science, information systems, business administration, and economics. In this research note, it is analyzed which pieces of this new “On-The-Fly Computing” ecosystem already exist and where additional, often significant research efforts are necessary.
  • 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.
  • ConferencePaper
    Cooperative Android App Analysis with CoDiDroid
    (Software Engineering 2021, 2021) Pauck, Felix; Wehrheim, Heike
    Novel Android app analysis tools as well as improved versions of available tools are frequently proposed. These proposed tools often tackle a specific single issue that cannot be handled with existing tools. Consequently, the best analysis possible should use the advantages of each and every tool. With CoDiDroid we present an analysis framework that allows to combine analysis tools such that the best out of each tool is used for a more comprehensive and more precise cooperative analysis. Our experimental results show indeed that CoDiDroid allows to setup cooperative analyses which are beneficial with respect to effectiveness, accuracy and scalability.
  • 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
    Jicer: Slicing Android Apps for Cooperative Analysis
    (Software Engineering 2023, 2023) Pauck, Felix; Wehrheim, Heike
    Slicing allows to identify which program parts influence or are influenced by a certain statement of a program. Hence, if we know which statement is potentially causing an issue we can slice accordingly to only inspect the slice while debugging. With Jicer, we proposed a slicer that can be used in a different context, namely cooperative Android app analysis. In combination with taint analysis tools, we employed Jicer to get more accurate results.
  • 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 Role of Artificial and Real Bug Fixes on the Training of Neural Bug Detectors
    (Software Engineering 2024 (SE 2024), 2024) Richter, Cedric; Wehrheim, Heike
  • Konferenzbeitrag
    Programs from proofs – Approach and applications
    (Software Engineering 2014, 2014) Wonisch, Daniel; Schremmer, Alexander; Wehrheim, Heike
  • Konferenzbeitrag
    Property-Driven Black-Box Testing of Numeric Functions
    (Software Engineering 2023, 2023) Sharma, Arnab; Melnikov, Vitalik; Hüllermeier, Eyke; Wehrheim, Heike
    In this work, we propose a property-driven testing mechanism to perform unit testing of functions performing numerical computations. Our approach, similar to the property-based testing technique, allows the tester to specify the requirements to check. Unlike property-based testing, the specification is then used to generate test cases in a targeted manner. Moreover, our approach works as a black-box testing tool, i.e. it does not require knowledge about the internals of the function under test. Therefore, besides on programmed numeric functions, we also apply our technique to machine-learned regression models. The experimental evaluation on a number of case studies shows the effectiveness of our testing approach.