Abstract
This tutorial presents LiquidHaskell, a usable formal verifier for Haskell programs. LiquidHaskell naturally integrates the specification of correctness properties in the development process. Moreover, verification is automatic, requiring no explicit proofs or complicated annotations. At the same time, the specification language is expressive and modular, allowing the user to specify correctness properties ranging from totality and termination to memory safety and safe resource (e.g., file) manipulation. Finally, LiquidHaskell has been used to verify more than 10,000 lines of real-world Haskell programs.
We will start the tutorial with an introduction of Liquid Types. Then, we will use LiquidHaskell to specify and verify basic program properties, like termination and safe list indexing. Finally, we will present advanced and new LiquidHaskell features including higher order reasoning and specification of stateful computations.
Tutorial objectives
use LiquidHaskell to specify and verify properties of Haskell programs including totality, termination and functional correctness.
Target audience
Static-verification enthusiasts, basic knowledge of Haskell, logic and type systems is encouraged.
Infrastructure Required
The tutorial will be uploaded online, so that the participants can follow via the online LiquidHaskell interface.
Niki Vazou
Niki Vazou is a Ph.D. candidate at University of California, San Diego, supervised by Ranjit Jhala. She works in the area of programming languages, with the goal of building usable program verifiers that will naturally integrate formal verification techniques into the mainstream software development chain.