Write a Blog >>

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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Refinement Types for Program Verification and SynthesisPLDI Tutorials at Vertex WS215
09:00
60m
Other
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
Refinement Types for Program Verification and Synthesis (cont'd)PLDI Tutorials at Vertex WS217
10:30
1h40m
Other
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