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 4.2.8 + AHUNTSIC [CC License]

info visites 3900530