Language-Integrated Verification - DLS Talk by Ranjit Jhala (UCSD)
Past Dates
In
Speaker: Dr. Ranjit Jhala, Professor, Computer Science Engineering, University of California, San Diego
Title: Language-Integrated Verification
Abstract:
The last few decades have seen tremendous strides in various technologies for reasoning about programs. However, we believe these technologies will only become ubiquitous if they can be seamlessly integrated within programming languages with mature compilers, libraries and tools so that programmers can use them continuously throughout the software development lifecycle (and not just as a means of post-facto validation.)
In this talk, we will describe how refinement types offer a path towards integrating verification into existing host languages. We show how refinements allow the programmer to extend specifications using types, to extend the analysis using SMT, and finally, to extend verification beyond automatically decidable logical fragments, by allowing programmers to interactively write proofs simply as functions in the host language.
Finally, we will describe some of the lessons learned while building and using the language integrated verifier LiquidHaskell. We will describe some problems that are considered hard in theory, but which turn out to be easy to address in practice, and we will describe other problems which might appear easy, but are actually giant roadblocks that will have to be removed to make verification broadly used.
Bio:
Ranjit Jhala is a professor of Computer Science and Engineering at the University of California, San Diego. He works on algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking, Program Analysis, and Automated Deduction, and Type Systems. He is proud to have written some of the most cited papers in Programming Languages over the last twenty years, and even more to have helped create several influential and award winning systems including the BLAST software model checker, RELAY race detector, MACE/MC distributed language and model checker, and Liquid Types. He was awarded ACM SIGPLAN's Robin Milner Young Researcher Award in 2018.
Host: William Bowman