%0 Conference Paper
%B Programming Languages and Systems - 25th European Symposium on Programming, {ESOP} 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
%D 2016
%T Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
%A Cláudio Belo Lourenço
%A Maria João Frade
%A Jorge Sousa Pinto
%E Peter Thiemann
%I Springer
%P 41–67
%R 10.1007/978-3-662-49498-1_3
%S Lecture Notes in Computer Science
%U http://dx.doi.org/10.1007/978-3-662-49498-1_3
%V 9632
%X <p>Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize pro- gram verification based on the translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct, and the subsequent generation of compact, indeed linear-size, verification conditions. Soundness and completeness proofs are given for the entire workflow, including the translation of an- notated programs to SA form. The formalization is based on a program logic that we show to be adaptation-complete. Although this important property has not, as far as we know, been established for any existing program verification tool, we believe that adaptation-completeness is one of the major motivations for the use of SA form as an intermediate lan- guage. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms.</p>
%Z <p>n/a</p>
%> https://haslab.uminho.pt/sites/default/files/mjf/files/camera_ready.pdf