Verimag

Seminar details

salle A. Turing CE4
25 February 2014 - 15h45
Definability of Accelerated Relations in a Theory of Arrays and its Applications
by Francesco Alberti from 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 | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 916103