The term “software verification” refers to the procedure of deciding the correctness of software with respect to (user-supplied or predefined) specifications. In general, software verification is an undecidable problem. Despite this undecidability, software verification is a very active research field with contributions of researchers from several areas such as theorem proving, static analysis, and automatic verification. The analysis techniques developed in these subareas are often complementary with respect to the type of software and specifications they can efficiently handle.

The objective of this Dagstuhl Seminar is to bring together people working in these different subareas to discuss and advance ways of having tools and techniques cooperate on the task of software verification. Specific focus shall be given to the exchange of information between tools. In particular, we plan to discuss the following questions:

1. Which kind of information can be exchanged?
2. How can we make tools provide their (partial) results about program correctness to other tools?
3. How can we make tools use (partial) results of other tools during their analysis?
4. How can we have tools check results of other tools?
5. Which formats are adequate for information exchange?

The overall goal of the seminar is to establish a new research area focused on information exchange in software verification, which will interconnect ideas, researchers, and tools across different communities working on software analysis and verification.

As the first step, we will identify the information currently produced, demanded, and exchanged by software analysis approaches and tools developed in each of these communities. Then we should compile the list of the current information exchange formats and processes used in the communities. The technical outcomes of the seminar can be a detailed inventory of existing format, a list of requirements of such formats, and an action plan with concrete steps leading to further development of these formats and the definition of new formats.

Creative Commons BY 4.0

Dirk Beyer, Marieke Huisman, Jan Strejcek, and Heike Wehrheim