Technical Reports

Andrei Voronkov, Iman Narasamdya
Proving Inter-Program Properties (2008)


Keywords: Assertion Function, Invariant, Translation Validation, Common Criteria Certification

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 two applications of the theory. One application is in the translation validation for optimizing compilers, and the other application is in the certification of smart-card application in the framework of Common Criteria. The latter application is part of an industrial project conducted at Verimag laboratory.

Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 3974365