Cooperative Software Verification

Teilnehmende:

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

Förderung:

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

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.

Publikationen

  • [article] bibtex
    J. Haltermann und 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, und H. Wehrheim, "Parallel Program Analysis on Path Ranges" CoRR, vol. abs/2402.11938.
    doi: 10.48550/ARXIV.2402.11938
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann, M. -, C. Richter, und 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 | Dokument aufrufen Dokument aufrufen
    M. Chalupa und 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, und 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 | Dokument aufrufen Dokument aufrufen
    D. Baier, D. Beyer, P. Chien, M. Jakobs, M. Jankola, M. Kettl, N. Lee, T. Lemberger, M. Lingsch-Rosenfeld, H. Wachowitz, und P. Wendler, "Software Verification with CPAchecker 3.0: Tutorial and User Guide" in Proc. Proc. FM, 2024.
  • D. Beyer, M. Kettl, und T. Lemberger, "Decomposing Software Verification Using Distributed Summary Synthesis" Proc. ACM Softw. Eng. vol. 1, iss. FSE.
    doi: 10.1145/3660766
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann, M. Jakobs, C. Richter, und H. Wehrheim, "Parallel Program Analysis via Range Splitting" in Proc. FASE, 2023.
    doi: 10.1007/978-3-031-30826-0_11
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann, M. -, C. Richter, und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer, S. Kanav, und H. Wachowitz, "CoVeriTeam Service: Verification as a Service" in Proc. Proc. ICSE, 2023.
    doi: 10.1109/ICSE-Companion58688.2023.00017
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    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 | Dokument aufrufen Dokument aufrufen
    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 | Dokument aufrufen Dokument aufrufen
    D. Beyer, J. Haltermann, T. Lemberger, und 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 | Dokument aufrufen Dokument aufrufen
    J. Haltermann und H. Wehrheim, "Machine Learning Based Invariant Generation: A Framework and Reproducibility Study" in Proc. ICST, 2022.
    doi: 10.1109/ICST53961.2022.00012
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    J. Haltermann und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer und 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 | Dokument aufrufen Dokument aufrufen
    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 | Dokument aufrufen Dokument aufrufen
    D. Beyer, S. Kanav, und 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 | Dokument aufrufen Dokument aufrufen
    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 und 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 | Dokument aufrufen Dokument aufrufen
    J. Haltermann und H. Wehrheim, "CoVEGI: Cooperative Verification via Externally Generated Invariants" in Proc. FASE, 2021.
    doi: 10.1007/978-3-030-71500-7_6
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    M. Jakobs und C. Richter, "CoVeriTest with Adaptive Time Scheduling (Competition Contribution)" in Proc. FASE, 2021.
    doi: 10.1007/978-3-030-71500-7_18
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    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 | Dokument aufrufen Dokument aufrufen
    C. Richter und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer, M. Jakobs, und 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 und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer und M. Jakobs, "CoVeriTest: Cooperative Verifier-Based Testing" in Proc. FASE, 2019.
    doi: 10.1007/978-3-030-16722-6_23
  • [inproceedings] bibtex | Dokument aufrufen Dokument aufrufen
    D. Beyer und 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 | Dokument aufrufen Dokument aufrufen
    D. Beyer, M. Jakobs, T. Lemberger, und H. Wehrheim, "Reducer-based construction of conditional verifiers" in Proc. ICSE, 2018.
    doi: 10.1145/3180155.3180259
(Stand: 12.07.2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page