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.
