A Single-Assignment Translation for Annotated Programs
Cl\'audio Belo Louren\c{c}o, Maria Jo\~ao Frade, Jorge Sousa Pinto
TL;DR
This paper introduces a translation method converting annotated While programs with loop invariants into a dynamic single-assignment language, ensuring soundness and completeness for program verification.
Contribution
It provides a novel translation technique that preserves correctness and completeness, facilitating verification in single-assignment languages.
Findings
Translation is sound and complete
Enables verification of annotated programs
Supports dynamic single-assignment languages
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 [6].
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Testing and Debugging Techniques · Formal Methods in Verification