@article {DBLP:journals/corr/LourencoFP16,
	title = {A Single-Assignment Translation for Annotated Programs},
	journal = {CoRR},
	volume = {abs/1601.00584},
	year = {2016},
	note = {<p>n/a</p>
},
	abstract = {<p>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.</p>
},
	url = {http://arxiv.org/abs/1601.00584},
	attachments = {https://haslab.uminho.pt/sites/default/files/mjf/files/satranslation.pdf},
	author = {Cl{\'a}udio Belo Louren{\c c}o and Maria Jo{\~a}o Frade and Jorge Sousa Pinto}
}