Cooperative Software Verification

Participants:

Heike Wehrheim, Jan Haltermann, Dirk Beyer (LMU Munich), Thomas Lemberger (LMU Munich)

Funding:

This project is funded by the German Research Council DFG (Cooperative Software Verification , 2019 - 2022, 2024 – 2027).

Cooperative Software Verification

Cooperative Software Verification

Software Verification

The aim of software verification is the assurance of high quality software, in particular absence of unintended and erroneous behaviour. Today, a range of different tools provide software analysis techniques, covering the whole area from static and dynamic analysis to model checking. All of these techniques have their individual strengths and weaknesses.

Cooperative Software Verification

The goal of this research project is the enhancement of precision and performance in software verification by cooperation between different verification tools and techniques.

Cooperative software verification requires (1) to enable exchange of information between verification tools and sound usage of such information, and (2) to learn how and when to cooperate. Cooperation targets the division of labour as to have every technology work on the tasks it is best at, but also aims at the increase of trust in the soundness of the analysis by having tools mutually check their results. The objective of our project is the development of a practical methodology of cooperative software verification based on a provably sound theory of cooperation. Our methodology targets safety verification.

Publications

  • [article] bibtex
    J. Haltermann and H. Wehrheim, "Exchanging information in cooperative software validation" Software and Systems Modeling.
    doi: 10.1007/s10270-024-01155-3
  • J. Haltermann, M. Jakobs, C. Richter, and H. Wehrheim, "Parallel Program Analysis on Path Ranges" CoRR, vol. abs/2402.11938.
    doi: 10.48550/ARXIV.2402.11938
  • [inproceedings] bibtex | Go to document Go to document
    J. Haltermann, M. -, C. Richter, and H. Wehrheim, "Ranged Program Analysis: A Parallel Divide-and-Conquer Approach for Software Verification" in Proc. Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024, 2024.
    doi: 10.18420/SW2024_52
  • [inproceedings] bibtex | Go to document Go to document
    M. Chalupa and C. Richter, "Bubaak-SpLit: Split what you cannot verify (Competition contribution)" in Proc. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, 2024.
    doi: 10.1007/978-3-031-57256-2_20
  • [inproceedings] bibtex
    D. Beyer, M. Kettl, and T. Lemberger, "Fault Localization on Verification Witnesses" in Proc. Proceedings of the 30th International Symposium on Model Checking Software (SPIN~2024, Luxembourg City, Luxembourg, April 10-11), 2024.
  • [inproceedings] bibtex | Go to document Go to document
    D. Baier, D. Beyer, P. Chien, M. Jakobs, M. Jankola, M. Kettl, N. Lee, T. Lemberger, M. Lingsch-Rosenfeld, H. Wachowitz, and P. Wendler, "Software Verification with CPAchecker 3.0: Tutorial and User Guide" in Proc. Proc. FM, 2024.
  • D. Beyer, M. Kettl, and T. Lemberger, "Decomposing Software Verification Using Distributed Summary Synthesis" Proc. ACM Softw. Eng. vol. 1, iss. FSE.
    doi: 10.1145/3660766
  • [inproceedings] bibtex | Go to document Go to document
    J. Haltermann, M. Jakobs, C. Richter, and H. Wehrheim, "Parallel Program Analysis via Range Splitting" in Proc. FASE, 2023.
    doi: 10.1007/978-3-031-30826-0_11
  • [inproceedings] bibtex | Go to document Go to document
    J. Haltermann, M. -, C. Richter, and H. Wehrheim, "Ranged Program Analysis via Instrumentation" in Proc. Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings, 2023.
    doi: 10.1007/978-3-031-47115-5_9
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, S. Kanav, and H. Wachowitz, "CoVeriTeam Service: Verification as a Service" in Proc. Proc. ICSE, 2023.
    doi: 10.1109/ICSE-Companion58688.2023.00017
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, "Competition on Software Verification and Witness Validation: SV-COMP 2023" in Proc. Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2023, Paris, France, April 22-27), 2023.
    doi: 10.1007/978-3-031-30820-8_29
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, "Software Testing: 5th Comparative Evaluation: Test-Comp 2023" in Proc. Proceedings of the 26th International Conference on Fundamental Approaches to Software Engineering (FASE~2023, Paris, France, April 22-27), 2023.
    doi: 10.1007/978-3-031-30826-0_17
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, J. Haltermann, T. Lemberger, and H. Wehrheim, "Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR" in Proc. ICSE, 2022.
    doi: 10.1145/3510003.3510064
  • [inproceedings] bibtex | Go to document Go to document
    J. Haltermann and H. Wehrheim, "Machine Learning Based Invariant Generation: A Framework and Reproducibility Study" in Proc. ICST, 2022.
    doi: 10.1109/ICST53961.2022.00012
  • [inproceedings] bibtex | Go to document Go to document
    J. Haltermann and H. Wehrheim, "Information Exchange Between Over- and Underapproximating Software Analyses" in Proc. SEFM, 2022.
    doi: 10.1007/978-3-031-17108-6_3
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer and S. Kanav, "CoVeriTeam: On-Demand Composition of Cooperative Verification Systems" in Proc. Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7, 2022.
    doi: 10.1007/978-3-030-99524-9_31
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, "Progress on Software Verification: SV-COMP 2022" in Proc. Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2022, Munich, Germany, April 2-7, 2022.
    doi: 10.1007/978-3-030-99527-0_20
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, S. Kanav, and C. Richter, "Construction of Verifier Combinations Based on Off-the-Shelf Verifiers" in Proc. Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7), 2022.
    doi: 10.1007/978-3-030-99429-7_3
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, "Advances in Automatic Software Testing: Test-Comp 2022" in Proc. Proceedings of the 25th International Conference on Fundamental Approaches to Software Engineering (FASE~2022, Munich, Germany, April 2-7), 2022.
    doi: 10.1007/978-3-030-99429-7_18
  • D. Beyer and M. Jakobs, "Cooperative Verifier-Based Testing with CoVeriTest" International Journal on Software Tools for Technology Transfer (STTT), vol. 23, iss. 3.
    doi: 10.1007/s10009-020-00587-8
  • [inproceedings] bibtex | Go to document Go to document
    J. Haltermann and H. Wehrheim, "CoVEGI: Cooperative Verification via Externally Generated Invariants" in Proc. FASE, 2021.
    doi: 10.1007/978-3-030-71500-7_6
  • [inproceedings] bibtex | Go to document Go to document
    M. Jakobs and C. Richter, "CoVeriTest with Adaptive Time Scheduling (Competition Contribution)" in Proc. FASE, 2021.
    doi: 10.1007/978-3-030-71500-7_18
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, "Status Report on Software Testing: Test-Comp 2021" in Proc. Proceedings of the 24th International Conference on Fundamental Approaches to Software Engineering (FASE~2021, Luxembourg, Luxembourg, March 27 - April 1), 2021.
    doi: 10.1007/978-3-030-71500-7_17
  • D. Beyer, "First International Competition on Software Testing" International Journal on Software Tools for Technology Transfer (STTT), vol. 23, iss. 6.
    doi: 10.1007/s10009-021-00613-3
  • [inproceedings] bibtex | Go to document Go to document
    C. Richter and H. Wehrheim, "Attend and Represent: A Novel View on Algorithm Selection for Software Verification" in Proc. ASE, 2020.
    doi: 10.1145/3324884.3416633
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer and H. Wehrheim, "Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework" in Proc. ISoLA, 2020.
    doi: 10.1007/978-3-030-61362-4_8
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer and M. Jakobs, "\sc FRed: Conditional Model Checking via Reducers and Folders" in Proc. Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18), 2020.
    doi: 10.1007/978-3-030-58768-0_7
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, M. Jakobs, and T. Lemberger, "Difference Verification with Conditions" in Proc. Proceedings of the 18th International Conference on Software Engineering and Formal Methods (SEFM~2020, Virtual, Netherlands, September 14-18), 2020.
    doi: 10.1007/978-3-030-58768-0_8
  • [inproceedings] bibtex
    D. Beyer and T. Lemberger, "TestCov: Robust Test-Suite Execution and Coverage Measurement" in Proc. Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019, San Diego, CA, USA, November 11-15), 2019.
    doi: 10.1109/ASE.2019.00105
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer and M. Jakobs, "CoVeriTest: Cooperative Verifier-Based Testing" in Proc. FASE, 2019.
    doi: 10.1007/978-3-030-16722-6_23
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer and T. Lemberger, "Conditional Testing - Off-the-Shelf Combination of Test-Case Generators" in Proc. Proceedings of the 17th International Symposium on Automated Technology for Verification and Analysis (ATVA~2019, Taipei, Taiwan, October 28-31), 2019.
    doi: 10.1007/978-3-030-31784-3_11
  • [inproceedings] bibtex | Go to document Go to document
    D. Beyer, M. Jakobs, T. Lemberger, and H. Wehrheim, "Reducer-based construction of conditional verifiers" in Proc. ICSE, 2018.
    doi: 10.1145/3180155.3180259
(Changed: 12 Jul 2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page