A Single-Assignment Translation for Annotated Programs

Citation:
Lourenço CB, Frade MJ, Pinto JS.  2016.  A Single-Assignment Translation for Annotated Programs. CoRR. abs/1601.00584

Abstract:

We present a translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct. We prove that the translation is sound and complete. This is a companion report to our paper Formalizing Single-assignment Program Verification: an Adaptation-complete Approach.

Notes:

n/a

Website

Citation Key:

DBLP:journals/corr/LourencoFP16
PreviewAttachmentSize
satranslation.pdf420.3 KB