Scope of the Workshop

The reliability of verification results is of the highest importance. 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, 2]. 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 [3]. 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:

The workshop should provoke the identification of weaknesses of the current witness formats and witness validation tools, and suggest improvements to the format, witness validation process, and increase the reliability of software verification in general. Hence, the research topics addressed by the workshop include:

References

  1. 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
  2. Ayaziová, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strejček, J.: Software verification witnesses 2.0. In: Proc. SPIN. Springer (2024). doi:10.1007/978-3-031-66149-5_11
  3. 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)
Marian Lingsch-Rosenfeld (LMU Munich, Germany)