Search

Your search keyword '"Jakobs, Marie-Christine"' showing total 102 results
Start Over Author "Jakobs, Marie-Christine"

Refine your results

more »

more »

more »
102 results on '"Jakobs, Marie-Christine"'

1. Software Verification with CPAchecker 3.0: Tutorial and User Guide (Extended Version)

Author

Baier, Daniel, Beyer, Dirk, Chien, Po-Chun, Jakobs, Marie-Christine, Jankola, Marek, Kettl, Matthias, Lee, Nian-Ze, Lemberger, Thomas, Lingsch-Rosenfeld, Marian, Wachowitz, Henrik, and Wendler, Philipp

Subjects
Computer Science - Software Engineering, Computer Science - Programming Languages, D.2.4, F.3.1, D.3.1, F.4.3
Abstract

This tutorial provides an introduction to CPAchecker for users. CPAchecker is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as BDDs, explicit values, intervals, memory graphs, and predicates, and many program-analysis and model-checking algorithms, such as abstract interpretation, bounded model checking, Impact, interpolation-based model checking, k -induction, PDR, predicate abstraction, and symbolic execution. This tutorial presents basic use cases for CPAchecker in formal software verification, focusing on its main verification techniques with their strengths and weaknesses. It also shows further use cases of CPAchecker for test-case generation and witness-based result validation. The envisioned readers are assumed to possess a background in automatic formal verification and program analysis, but prior knowledge of CPAchecker is not required. This tutorial and user guide is based on CPAchecker in version 3.0. This user guide's latest version and other documentation are available at https://cpachecker.sosy-lab.org/doc.php., Comment: 39 pages, 17 figures, 6 tables

Published
2024

2. Parallel Program Analysis on Path Ranges

Author

Haltermanna, Jan, Jakobs, Marie-Christine, Richter, Cedric, and Wehrheim, Heike

Subjects
Computer Science - Software Engineering
Abstract

Symbolic execution is a software verification technique symbolically running programs and thereby checking for bugs. Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. Due to the parallelism, verification is accelerated and hence scales to larger programs. In this paper, we discuss a generalization of ranged symbolic execution to arbitrary program analyses. More specifically, we present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel. Our approach in particular allows to run different analyses on different program parts. We have implemented this generalization on top of the tool CPAchecker and evaluated it on programs from the SV-COMP benchmark. Our evaluation shows that verification can benefit from the parallelisation of the verification task, but also needs a form of work stealing (between analyses) as to become efficient, Comment: under submission

Published
2024
Full Text
View/download PDF

3. Incorporating Data Dependencies and Properties in Difference Verification with Conditions (Technical Report)

Author

Jakobs, Marie-Christine and Pollandt, Tim

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages, D.2.4, I.2.2
Abstract

Software changes frequently. To efficiently deal with such frequent changes, software verification tools must be incremental. Most of today's approaches for incremental verification consider one specific verification approach. One exception is difference verification with conditions recently proposed by Beyer et al. Its underlying idea is to determine an overapproximation of those modified execution paths that may cause a new property violation, which does not exist in the unchanged program, encode the determined paths into a condition, and use the condition to restrict the verification to the analysis of those determined paths. To determine the overapproximation, Beyer et al. propose a syntax-based difference detector that adds any syntactical path of the modified program that does not exist in the original program into the overapproximation. This paper provides a second difference detector diffDP, which computes a more precise overapproximation by taking data dependencies and program properties into account when determining the overapproximation of those modified execution paths that may cause a new property violation. Our evaluation indeed shows that our more precise difference detector improves the effectiveness and efficiency of difference verification with condition on several tasks.

Published
2023

4. Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution)

Author

Barth, Max, Dietsch, Daniel, Heizmann, Matthias, Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Beyer, Dirk, editor, and Cavalcanti, Ana, editor

Published
2024
Full Text
View/download PDF

9. Ranged Program Analysis via Instrumentation

Author

Haltermann, Jan, Jakobs, Marie-Christine, Richter, Cedric, Wehrheim, Heike, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Ferreira, Carla, editor, and Willemse, Tim A. C., editor

Published
2023
Full Text
View/download PDF

10. Parallel Program Analysis via Range Splitting

Author

Haltermann, Jan, Jakobs, Marie-Christine, Richter, Cedric, Wehrheim, Heike, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Lambers, Leen, editor, and Uchitel, Sebastián, editor

Published
2023
Full Text
View/download PDF

11. PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)

Author

Jakobs, Marie-Christine

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages
Abstract

Refactorings must not alter the program's functionality. However, not all refactorings fulfill this requirement. Hence, one must explicitly check that a refactoring does not alter the functionality. Since one rarely has a formal specification of the program's behavior, we utilize the original program as functional specification. Then, we check whether the original and refactored program are functionally equivalent. To this end, we apply a common idea and reduce equivalence checking to program verification. To increase efficiency, our equivalence checker PEQcheck constructs one verification task per refactored code segment instead of one per function as typically done by prior work. In addition, PEQcheck considers the context of the code segments. For instance, only variables that are modified and live are required to be equivalent and read-only variables may be shared between original and refactored code segments. We show that PEQcheck is sound.Moreover, our evaluation testifies that the localized and context-aware checking performed by \peqcheck can indeed be beneficial.

Published
2021

14. Automatic Test-Case Generation with CoVeriTest (Extended Abstract)

Author

Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Kovács, Laura, editor, and Meinke, Karl, editor

Published
2022
Full Text
View/download PDF

15. Reusing Predicate Precision in Value Analysis

Author

Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, ter Beek, Maurice H., editor, and Monahan, Rosemary, editor

Published
2022
Full Text
View/download PDF

16. PEQtest: Testing Functional Equivalence

Author

Jakobs, Marie-Christine, Wiesner, Maik, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Johnsen, Einar Broch, editor, and Wimmer, Manuel, editor

Published
2022
Full Text
View/download PDF

18. Cooperative verifier-based testing with CoVeriTest

Author

Beyer, Dirk, Jakobs, Marie-Christine, Beyer, Dirk, and Jakobs, Marie-Christine

Abstract

Testing is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15%).

Published
2024

19. CoVeriTest: interleaving value and predicate analysis for test-case generation

Author

Jakobs, Marie-Christine and Jakobs, Marie-Christine

Abstract

Verification techniques are well-suited for automatic test-case generation. They basically need to check the reachability of every test goal and generate test cases for all reachable goals. This is also the basic idea of our CoVeriTest submission. However, the set of test goals is not fixed in CoVeriTest , instead we can configure the set of test goals. For Test-Comp’19, we support the set of all __VERIFIER_error() calls as well as the set of all branches. Thus, we can deal with the two test specifications considered in Test-Comp’19. Since the tasks in Test-Comp are diverse and verification techniques have different strengths and weaknesses, we also do not stick to a single verification technique, but use a hybrid approach that combines multiple techniques. More concrete, CoVeriTest interleaves different verification techniques and allows to configure the cooperation (i.e., information exchange and time limits). To choose from a large set of verification techniques, CoVeriTest is integrated into the analysis framework CPAchecker. For the competition, we interleave CPAchecker’s value and predicate analysis and let both analyses resume their analysis performed in the previous iteration.

Published
2024

20. PatEC: Pattern-Based Equivalence Checking

Author

Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Laarman, Alfons, editor, and Sokolova, Ana, editor

Published
2021
Full Text
View/download PDF

21. Verifying Pipeline Implementations in OpenMP

Author

Wiesner, Maik, Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Laarman, Alfons, editor, and Sokolova, Ana, editor

Published
2021
Full Text
View/download PDF

22. CoVeriTest with Adaptive Time Scheduling (Competition Contribution)

Author

Jakobs, Marie-Christine, Richter, Cedric, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Guerra, Esther, editor, and Stoelinga, Mariëlle, editor

Published
2021
Full Text
View/download PDF

23. Predicting Rankings of Software Verification Competitions

Author

Czech, Mike, Hüllermeier, Eyke, Jakobs, Marie-Christine, and Wehrheim, Heike

Subjects
Computer Science - Learning, Computer Science - Software Engineering, I.2.6, D.2.4
Abstract

Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task. In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions).

Published
2017

28. A Unifying Framework for Dynamic Monitoring and a Taxonomy of Optimizations

Author

Jakobs, Marie-Christine, Mantel, Heiko, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Margaria, Tiziana, editor

Published
2020
Full Text
View/download PDF

29. FRed: Conditional Model Checking via Reducers and Folders

Author

Beyer, Dirk, Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, de Boer, Frank, editor, and Cerone, Antonio, editor

Published
2020
Full Text
View/download PDF

30. Difference Verification with Conditions

Author

Beyer, Dirk, Jakobs, Marie-Christine, Lemberger, Thomas, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, de Boer, Frank, editor, and Cerone, Antonio, editor

Published
2020
Full Text
View/download PDF

32. HybridTiger: Hybrid Model Checking and Domination-based Partitioning for Efficient Multi-Goal Test-Suite Generation (Competition Contribution)

Author

Ruland, Sebastian, Lochau, Malte, Jakobs, Marie-Christine, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Wehrheim, Heike, editor, and Cabot, Jordi, editor

Published
2020
Full Text
View/download PDF

33. Deriving approximation tolerance constraints from verification runs

Author

Isenberg, Tobias, Jakobs, Marie-Christine, Pauck, Felix, and Wehrheim, Heike

Subjects
Computer Science - Software Engineering, D.2.4, F.3.1
Abstract

Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing for hardware which only carries out "approximately correct" calculations. For software verification, this challenges the validity of verification results for programs run on approximate hardware. In this paper, we present a novel approach to examine program correctness in the context of approximate computing. In contrast to all existing approaches, we start with a standard program verification and compute the allowed tolerances for AC hardware from that verification run. More precisely, we derive a set of constraints which - when met by the AC hardware - guarantees the verification result to carry over to AC. Our approach is based on the framework of abstract interpretation. On the practical side, we furthermore (1) show how to extract tolerance constraints from verification runs employing predicate abstraction as an instance of abstract interpretation, and (2) show how to check such constraints on hardware designs. We exemplify our technique on example C programs and a number of recently proposed approximate adders.

Published
2016

35. When Are Software Verification Results Valid for Approximate Hardware?

Author

Isenberg, Tobias, Jakobs, Marie-Christine, Pauck, Felix, Wehrheim, Heike, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Beyer, Dirk, editor, and Keller, Chantal, editor

Published
2019
Full Text
View/download PDF

36. CoVeriTest: Cooperative Verifier-Based Testing

Author

Beyer, Dirk, Jakobs, Marie-Christine, Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Hähnle, Reiner, editor, and van der Aalst, Wil, editor

Published
2019
Full Text
View/download PDF

41. JMCTest: Automatically Testing Inter-Method Contracts in Java

Author

Börding, Paul, Haltermann, Jan, Jakobs, Marie-Christine, Wehrheim, Heike, Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Weikum, Gerhard, Series Editor, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Medina-Bulo, Inmaculada, editor, Merayo, Mercedes G., editor, and Hierons, Robert, editor

Published
2018
Full Text
View/download PDF

46. PART: From Partial Analysis Results to a Proof Witness

Author

Jakobs, Marie-Christine, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Cimatti, Alessandro, editor, and Sirjani, Marjan, editor

Published
2017
Full Text
View/download PDF

47. Compact Proof Witnesses

Author

Jakobs, Marie-Christine, Wehrheim, Heike, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Barrett, Clark, editor, Davies, Misty, editor, and Kahsai, Temesghen, editor

Published
2017
Full Text
View/download PDF

50. Just Test What You Cannot Verify!

Author

Czech, Mike, Jakobs, Marie-Christine, Wehrheim, Heike, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Egyed, Alexander, editor, and Schaefer, Ina, editor

Published
2015
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results