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

info visites 1877756