Verimag

Détails sur le séminaire

salle A. Turing CE4
25 février 2014 - 15h45
Definability of Accelerated Relations in a Theory of Arrays and its Applications
par Francesco Alberti de USI Lugano



Abstract: We show that accelerations (i.e., transitive closures) of a class of guarded assignments for arrays are definable via \\\\exists*\\\\forall*-first order formulae, and apply this result in the verification of programs with arrays.




Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 876903