Scope of the Workshop
The reliability of verification results is of the highest importance for the CAV community. The workshop focuses on the reliability of the results of software-verification tools. Software-verification tools sometimes produce incorrect answers, which can be a false alarm or a wrong claim of correctness. To increase the reliability of verification results, many verifiers now accompany their answers by witnesses in an interoperable standard format [1]. There exist witness validators that can examine the witnesses and potentially confirm the verification results. This year, the community changed the semantics of the witness validation such that a witness can be also refuted [2]. Witness refutation indicates that the corresponding verification result is unreliable. In spite of the fast progress in the area of software-verification reliability based on witnesses, there are still many important topic, in particular:
- How to improve or guarantee the reliability of witness validators.
- Expressiveness, conciseness, and unambiguity of witness description formats.
- Reliability of software-verification results in general.
- Formats for representation of software-verification witnesses.
- Methods, techniques, and tools for sound validation and refutation of software-verification witnesses.
Keynotes
VeWit hosts the following two keynotes:
- Matthias Heizmann and Andreas Podelski, University of Freiburg, Germany
- Heike Wehrheim, University of Oldenburg, Germany
References
- D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, T. Lemberger, M. Tautschnig: Verification Witnesses. ACM Trans. Softw. Eng. Methodol. 31(4): 57:1-57:69 (2022). doi:10.1145/3477579
- D. Beyer and J. Strejček: Case Study on Verification-Witness Validators: Where We Are and Where We Go. Proc. SAS 2022. doi:10.1007/978-3-031-22308-2_8
Organizers
Dirk Beyer (LMU Munich, Germany)
Jan Strejček (Masaryk University, Czechia)