Abstract
We develop foundations for proving properties relating two programs. Our formalization is based on a suitably adapted notion of program invariant for a single program. First, we give an abstract formulation of the theory of program invariants based on the notion of assertion function: a function that assigns assertions to program points. Then, we develop this abstract notion further so that it can be used to prove properties between two programs. We describe an application of the theory to proving program properties in translation validation. © 2009 Springer.
Author supplied keywords
Cite
CITATION STYLE
Voronkov, A., & Narasamdya, I. (2009). Inter-program properties. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5673 LNCS, pp. 343–359). https://doi.org/10.1007/978-3-642-03237-0_23
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
