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 | Plan du site | Site réalisé avec SPIP 3.2.15 + AHUNTSIC [CC License]

info visites 1862055