Titolo: Foundational certification of data-flow analyses

Relatore: Tarmo Uustalu
                Institute of Cybernetics, Tallinn University of Technology
(Joint work with Maria João Frade and Ando Saabas.)

Abstract: Laud et al. have demonstrated that classical data-flow analyses,
such as live variables analysis, available expressions analysis etc., are
usefully specifiable as type systems. These are sound and, in the case of
distributive analysis frameworks, complete wrt. appropriate natural semantics
on abstract properties (the underlying abstract interpretations). Applications
include certification of analyses by type derivations and optimization of
programs and "optimization" of Hoare triple derivations alongside programs
based on such certificates. On the example of live variables analysis, we show
that analysis type systems are applied versions of more foundational Hoare
logics describing either the same property semantics as the type system or a
more basic natural semantics on transition traces of a suitable kind. The
rules of a type system are derivable in the Hoare logic for the abstract
property semantics and those in turn in the Hoare logic for the transition
trace semantics. This reduction of the burden of trusting the certification
vehicle can be compared to foundational proof-carrying code, where
general-purpose program logics are preferred to special-purpose type systems
and universal logic to program logics.

Rif. Miculan

--  Marino Miculan - Department of Mathematics and Computer Science
University of Udine  - via delle Scienze 206, 33100 Udine - Italy
vox: +39-043255-8486 - fax: +39-043255-8499 - mob: +39-3292606452
mail:miculan at dimi uniud it  http://www.dimi.uniud.it/~miculan/