BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Peter Müller - Specification and Verification of Closures
DTSTART:20100330T161500
DTSTAMP:20260511T163211Z
UID:99788e30a029f1b35499d6527a0beaf90b916c48f25fc08056577f83
CATEGORIES:Conferences - Seminars
DESCRIPTION:Peter Müller (ETH Zürich)\nClosures\, first-class citizen pr
 ocedures that are able to capture their lexical environment\, increase the
  expressiveness of object-oriented languages such as C#\, Scala\, and vari
 ous dynamic languages. However\, closures make program specification and v
 erification more difficult. For instance\, a verification methodology must
  allow specifications to describe the behavior of one method relatively to
  the specification of another method passed as argument\, and it must allo
 w specifications to describe the behavior of a closure without exposing it
 s captured state. This paper presents a modular specification and verifica
 tion methodology for closures. Our solution is based on first-order logic 
 and\, thus\, well suited for automatic verification with SMT solvers. We h
 ave verified a series of interesting examples that cover the main applicat
 ions of closures such as delegation patterns and  even the creation of cus
 tom control flow.
LOCATION:INM 010
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR