TY - GEN
T1 - Preserving user proofs across specification changes
AU - Bobot, François
AU - Filliâtre, Jean Christophe
AU - Marché, Claude
AU - Melquiond, Guillaume
AU - Paskevich, Andrei
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2014.
PY - 2014/1/1
Y1 - 2014/1/1
N2 - In the context of deductive program verification, both the specification and the code evolve as the verification process carries on. For instance, a loop invariant gets strengthened when additional properties are added to the specification. This causes all the related proof obligations to change; thus previous user verifications become invalid. Yet it is often the case that most of previous proof attempts (goal transformations, calls to interactive or automated provers) are still directly applicable or are easy to adjust. In this paper, we describe a technique to maintain a proof session against modification of verification conditions. This technique is implemented in the Why3 platform. It was successfully used in developing more than a hundred verified programs and in keeping them up to date along the evolution of Why3 and its standard library. It also helps out with changes in the environment, e.g. prover upgrades.
AB - In the context of deductive program verification, both the specification and the code evolve as the verification process carries on. For instance, a loop invariant gets strengthened when additional properties are added to the specification. This causes all the related proof obligations to change; thus previous user verifications become invalid. Yet it is often the case that most of previous proof attempts (goal transformations, calls to interactive or automated provers) are still directly applicable or are easy to adjust. In this paper, we describe a technique to maintain a proof session against modification of verification conditions. This technique is implemented in the Why3 platform. It was successfully used in developing more than a hundred verified programs and in keeping them up to date along the evolution of Why3 and its standard library. It also helps out with changes in the environment, e.g. prover upgrades.
U2 - 10.1007/978-3-642-54108-7_10
DO - 10.1007/978-3-642-54108-7_10
M3 - Conference contribution
AN - SCOPUS:84927642115
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 191
EP - 201
BT - Verified Software
A2 - Cohen, Ernie
A2 - Rybalchenko, Andrey
A2 - Rybalchenko, Andrey
PB - Springer Verlag
T2 - 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013
Y2 - 17 May 2013 through 19 May 2013
ER -