BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:PSync \, a domain specific language based on the Heard-Of model
DTSTART:20151222T161500
DTEND:20151222T171500
DTSTAMP:20260502T190051Z
UID:9c71609932e04f47061ed15b22ee1d035706fa8a69d9d94f16c4ef94
CATEGORIES:Conferences - Seminars
DESCRIPTION:Damien Zufferey\nFault-tolerant distributed algorithms play an
  important role in many critical/high-availability applications. These alg
 orithms are notoriously difficult to implement correctly\, due to asynchro
 nous communication and the occurrence of faults\, such as the network drop
 ping messages or computers crashing.\n    We introduce PSync\, a domain
  specific language based on the Heard-Of model\, which views asynchronous 
 faulty systems as synchronous ones with an adversarial environment that si
 mulates asynchrony and faults by dropping messages. We define a runtime sy
 stem for PSync that efficiently executes on asynchronous networks. We form
 alise the relation between the runtime system and PSync in terms of observ
 ational refinement. This high-level synchronous abstraction introduced by 
 PSync simplifies the design and implementation of fault-tolerant distribut
 ed algorithms and enables automated formal verification.\n    We have i
 mplemented an embedding of PSync in the Scala programming language with a 
 runtime system for partially synchronous networks. We show the applicabili
 ty of PSync by implementing several important fault-tolerant distributed a
 lgorithms and we compare the implementation of consensus algorithms in PSy
 nc against implementations in other languages in terms of code size\, runt
 ime efficiency\, and verification.\n    This is joint work with Cezara 
 Dragoi and Tom Henzinger.\nDamien Zufferey is a Postdoctoral researcher in
  Martin Rinard's group at MIT CSAIL since Octorber 2013. Before moving to 
 MIT\, he obtained a PhD at the Institute of Science and Technology Austria
  (IST Austria) under supervision of Thomas A. Henzinger in September 2013 
 and a Master in computer science from EPFL in 2009. He is interested in im
 proving software reliability by developing theoretical models\, building a
 nalysis tools\, and giving the programmer the appropriate language constru
 cts. He is particularly interested in the study of complex concurrent syst
 ems. His research lies at the intersection of formal methods and programmi
 ng languages.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR