BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium : Type-Driven Program Synthesis
DTSTART:20170403T101500
DTEND:20170403T113000
DTSTAMP:20260430T062546Z
UID:694fea9c6fc7d8eec3f9ba3f07e8290d63d89e6f21eb62bafe47fe58
CATEGORIES:Conferences - Seminars
DESCRIPTION:By : Nadia Polikarpova - Massachusetts Institute of Technology
 \nIC Faculty candidate\n\nAbstract :\nModern programming languages safegua
 rd developers from many typical errors\, yet more subtle errors—such as 
 violations of security policies—still plague software. Program synthesis
  has the potential to eliminate such errors\, by generating executable cod
 e from concise and intuitive high-level specifications. Traditionally\, pr
 ogram synthesis failed to scale to specifications that encode complex beha
 vioral properties of software: these properties are notoriously hard to ch
 eck even for a given program\, and so it’s not surprising that finding t
 he right program within a large space of candidates has been considered ve
 ry challenging. My work tackles this challenge through the design of synth
 esis-friendly program verification mechanisms\, which are able to check a 
 large set of candidate programs against a complex specification at once\, 
 whereby efficiently pruning the search space.\n \nBased on this principle
 \, I developed Synquid\, a program synthesizer that accepts specifications
  in the form of expressive types and uses a specialized type checker as it
 s underlying verification mechanism. Synquid is the first synthesizer powe
 rful enough to automatically discover provably correct implementations of 
 complex data structure manipulations\, such as insertion into Red-Black Tr
 ees and AVL Trees\, and normal-form transformations on propositional formu
 las. Each of these programs is synthesized in under a minute. Going beyond
  textbook algorithms\, I created a language called Lifty\, which uses type
 -driven synthesis to automatically rewrite programs that violate informati
 on flow policies. In our case study\, Lifty was able to enforce all requir
 ed policies in a prototype conference management system.\n\nBio :\nNadia P
 olikarpova is a postdoctoral researcher at the MIT Computer Science and Ar
 tificial Intelligence Lab\, interested in helping programmers build secure
  and reliable software. She completed her PhD at ETH Zurich. For her disse
 rtation she developed tools and techniques for automated formal verificati
 on of object-oriented libraries\, and created the first fully verified gen
 eral-purpose container library\, receiving the Best Paper Award at the Int
 ernational Symposium on Formal Methods. During her doctoral studies\, Nadi
 a was an intern at MSR Redmond\, where she worked on verifying real-world 
 implementations of security protocols. At MIT\, Nadia has been applying fo
 rmal verification to automate various critical and error-prone programming
  tasks.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR