Software verification has recently made enormous progress
due to the development of novel verification methods and the speed-up
of supporting technologies like SMT solving. To keep software verifi-
cation tools up to date with these advances, tool developers keep on
integrating newly designed methods into their tools, almost exclusively
by re-implementing the method within their own framework. While this
allows for a conceptual re-use of methods, it nevertheless requires novel
implementations for every new technique.
In this paper, we employ cooperative verification in order to avoid re-
implementation and enable usage of novel tools as black-box components
in verification. Specifically, cooperation is employed for the core ingre-
dient of software verification which is invariant generation. Finding an
adequate loop invariant is key to the success of a verification run. Our
framework named CoVEGI allows a master verification tool to delegate
the task of invariant generation to one or several specialized helper in-
variant generators. Their results are then utilized within the verification
run of the master verifier, allowing in particular for crosschecking the va-
lidity of the invariant. We experimentally evaluate our framework on an
instance with two masters and three different invariant generators using
a number of benchmarks from SV-COMP 2020. The experiments show
that the use of CoVEGI can increase the number of correctly verified
tasks without increasing the used resources

CoVEGI: Cooperative Verification via Externally Generated Invariants

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme