BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Monday Seminar : "Algorithmic Software Verification for Data St
 ructures"
DTSTART:20110321T161500
DTSTAMP:20260503T082716Z
UID:df100b1c67c843187a78115f167edcc52d3c8d51818f875aab281d6b
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr. Pavol Cerny\, IST Austria - IC Faculty candidate\nAbstract
  : Algorithmic methods for software verification have been very successful
  in verifying sequential properties of control-oriented programs such as d
 evice drivers. The main challenges currently include verification of concu
 rrent and data-oriented programs. In particular\, concurrent data structur
 es are notoriously difficult to implement correctly. Algorithmic software 
 verification is an especially effective analysis method in this case\, as 
 the difficulty of reasoning about these implementations does not stem from
  the number of variables or the program size\, but rather from the large n
 umber of possible interleavings. In this talk\, I will focus on algorithms
  for verifying properties of both sequential and concurrent programs acces
 sing heap-based data structures. First\, I will present streaming string t
 ransducers\, a robust\, expressive\, and analyzable model of programs. The
  pre/post condition checking and equivalence checking problems are decidab
 le for streaming string transducers\, and the expressiveness of the model 
 is the same as that of MSO transductions. Second\, I will show how these r
 esults lead to algorithms for assertion checking and for checking function
 al equivalence for a class of sequential programs. This class includes com
 mon list-manipulating routines\, such as insert\, delete\, and reverse. Th
 ird\, I will present an algorithm for verifying linearizability for a clas
 s of concurrent programs which covers many of the common implementation te
 chniques\, such as fine-grained locking\, and optimistic\, lazy\, and lock
 -free synchronization. The tool COLT implements the algorithm\, and was us
 ed to verify (and find bugs in) a representative sample of Java implementa
 tions of the concurrent set data structure. Bio: Pavol Cerny is a postdoct
 oral researcher at IST Austria. He obtained his PhD in Computer Science fr
 om the University of Pennsylvania in 2009 and a DEA diploma from Ecole nor
 male superieure\, Paris\, France in 2003. His current research interests a
 re in formal methods and programming languages\, in particular in algorith
 mic verification for concurrent software and in quantitative program synth
 esis. He also worked on a new programming model for data parallel programs
 \, on verification of software security\, and on security analysis of elec
 tronic voting machines.
LOCATION:INM 202
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR