부산대학교 도서관

Summary: ``Deductive verification tools typically rely on theconversion of code to a single-assignment (SA) form. In this paper weformalize program verification based on the translation of {\it While}programs annotated with loop invariants into a dynamicsingle-assignment language with a dedicated iterating construct, andthe subsequent generation of compact, indeed linear-size, verificationconditions. Soundness and completeness proofs are given for the entireworkflow, including the translation of annotated programs to SA form.The formalization is based on a program logic that we show to be {\it adaptation-complete}. Although this important property has not, as faras we know, been established for any existing program verificationtool, we believe that adaptation-completeness is one of the majormotivations for the use of SA form as an intermediate language. Ourresults here show that indeed this allows for the tools to achieve themaximum degree of adaptation when handling subprograms.''