Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/4534
Title: Formalizing single-assignment program verification: An adaptation-complete approach
Authors: Cláudio Belo Lourenço
Maria João Frade
Jorge Sousa Pinto
Issue Date: 2016
Abstract: Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize program 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 annotated 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 adaptationcompleteness is one of the major motivations for the use of SA form as an intermediate language. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms. © Springer-Verlag Berlin Heidelberg 2016.
URI: http://repositorio.inesctec.pt/handle/123456789/4534
http://dx.doi.org/10.1007/978-3-662-49498-1_3
metadata.dc.type: conferenceObject
Publication
Appears in Collections:HASLab - Articles in International Conferences

Files in This Item:
File Description SizeFormat 
P-00K-9TQ.pdf483.83 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.