Refinement Types for Program Verification and Synthesis
Thu 22 Jun 2017 10:30 - 12:10 at Vertex WS217 - Refinement Types for Program Verification and Synthesis (cont'd)
In this tutorial you will learn how refinement types—types decorated with decidable predicates—can be used for automated SMT-based program analysis and synthesis. The presentation will focus on two programming tools we have developed. The first one is LiquidHaskell, a program verifier that relies on refinement type inference to analyze advanced language features like higher order functions, polymorphism, and algebraic data types, leading to practical verification of real-world Haskell code, including safe pointer arithmetic, array indexing and functional correctness of AVL/Red-Black trees. The second tool is Synquid, a program synthesizer that generates recursive functional programs that provably satisfy a given specification in the form of a refinement type. The tutorial will include hands-on exercises, so bring your laptops!
Thu 22 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mOther | Refinement Types for Program Verification and Synthesis PLDI Tutorials Niki Vazou University of Maryland, Nadia Polikarpova MIT CSAIL, USA, Ranjit Jhala University of California at San Diego, USA Media Attached | ||
10:30 - 12:10 | |||
10:30 1h40mOther | Refinement Types for Program Verification and Synthesis PLDI Tutorials Niki Vazou University of Maryland, Nadia Polikarpova MIT CSAIL, USA, Ranjit Jhala University of California at San Diego, USA Media Attached | ||