Presenter
Márk Somorjai
LMU Munich
Authors
Paulína Ayaziová, Dirk Beyer, Marie-Christine Jakobs, Martin Jonáš, Marian Lingsch-Rosenfeld, Jindřich Sedláček, Márk Somorjai, Jan Strejček
Abstract
Program changes made during the evolution of software may invalidate verification results, therefore, every program version needs to be (re)verified. Performing a complete reverification, however, is too costly to keep up with today’s frequent program changes. In 2013, precision reuse was introduced as a means to speed up the iterative computation of an abstraction level that is appropriate for verification. In an external reproduction and replication study, we examine the major claims and observations of the original study and find that they mostly remain valid and carry over, but the benefits of precision reuse are less significant. We further observe that the format used in the original study has limited use for exchange, as it contains verifier-specific elements. Thus, we additionally propose a verifier-independent exchange format for precisions, and evaluate its utility in 3 abstraction-based verification tools. Our evaluation shows that cooperation between verifiers by exchanging precisions can improve verification performance, solving tasks that could not be solved by any of the verifiers alone.
Slides
TBA