n/a
}, pages = {41{\textendash}67}, publisher = {Springer}, organization = {Springer}, abstract = {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.
}, doi = {10.1007/978-3-662-49498-1_3}, url = {http://dx.doi.org/10.1007/978-3-662-49498-1_3}, attachments = {https://haslab.uminho.pt/sites/default/files/mjf/files/camera_ready.pdf}, author = {Cl{\'a}udio Belo Louren{\c c}o and Maria Jo{\~a}o Frade and Jorge Sousa Pinto}, editor = {Peter Thiemann} }