Write a Blog >>
PLDI 2017
Sun 18 - Fri 23 June 2017 Barcelona, Spain

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 Jun

pldi-2017-workshops-and-tutorials
09:00 - 12:00: Tutorials - Refinement Types for Program Verification and Synthesis at PLDI-E
pldi-2017-workshops-and-tutorials149811480000009:00 - 12:00
Other
Media Attached