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!

Conference Day
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 VazouUniversity of Maryland, Nadia PolikarpovaMIT CSAIL, USA, Ranjit JhalaUniversity 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 VazouUniversity of Maryland, Nadia PolikarpovaMIT CSAIL, USA, Ranjit JhalaUniversity of California at San Diego, USA
Media Attached