BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Relational Analysis of Non-deterministic Integer Programs 
DTSTART:20110620T141500
DTSTAMP:20260407T230520Z
UID:9847cb86ec8c0f1cf29d0c7638d3e1246112a9ac92e9230c4f13b3e0
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr Radu Iosif\, Véermag\, CNRS and University of Grenoble\nAu
 tomatic inference of function summaries is the key to compositional verifi
 cation of numerical programs. In the first part of this talk I will presen
 t an algorithm for verifying hierarchical non-recursive programs\, based o
 n an efficient computation of transitive closures for several classes of p
 rogram loops: difference bounds\, octagonal and\nfinite monoid affine rela
 tions.\n\nOn the theoretical side\, this provides a common solution to the
  acceleration problem\, for all these three classes of relations. In pract
 ice\, according to our experiments\, the new method performs up to four or
 ders of magnitude better than the previous ones for the first two classes.
  \n\nIn the second part of the talk\, I explain how transitive closure com
 putation combines with other methods (quantifier elimination\, abstraction
 \, etc.) in order to provide a framework for the analysis of such systems.
  These ideas led us to the implementation of the FLATA tool.\n\nJoint work
  with Marius Bozga and Filip Konecny.  \n\nProf. Iosif's homepage
LOCATION:BC 01 https://plan.epfl.ch/?room==BC%2001
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR