Date & Time:
January 22, 2019 2:30 pm – 3:30 pm
Location:
Crerar 390, 5730 S. Ellis Ave., Chicago, IL,
01/22/2019 02:30 PM 01/22/2019 03:30 PM America/Chicago Ranjit Jhala (UCSD) – Language-Integrated Verification Crerar 390, 5730 S. Ellis Ave., Chicago, IL,

Language-Integrated Verification

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.

Host: Ravi Chugh

Ranjit Jhala

Professor of Computer Science and Engineering, University of California, San Diego

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 has written some of the most cited papers in Programming Languages over the last two decades and has created 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.

Related News & Events

UChicago CS News

UChicago Hosts NSF Workshop on Frontiers of Quantum Advantage

Aug 15, 2022
UChicago CS News

New 2022-23 CS Faculty Add Expertise in Linguistics, Visualization, Economics, and Data Science Education

Aug 11, 2022
In the News

UChicago Co-Leads $10 Million NSF Institute on Foundations of Data Science

Aug 09, 2022
In the News

Bill Fefferman Comments on New Standards for Quantum-Proof Cryptography

Jul 07, 2022
UChicago CS News

UChicago London Colloquium Features Data Science, Quantum Research

Jul 01, 2022
UChicago CS News

Faculty Bill Fefferman and Chenhao Tan Receive Google Research Scholar Awards

Jun 21, 2022
UChicago CS News

First-Year PhD Student Co-Authors Outstanding Paper Award Winner at TQC 2022

Apr 28, 2022
UChicago CS News

Concurrency Bug Research by Prof. Shan Lu Receives ASPLOS Influential Paper Award

Mar 29, 2022
In the News

Quanta Magazine Features Prof. Bill Fefferman’s Work on Quantum Algorithms

Jan 20, 2022
UChicago CS News

In-Fridge Controller Could Scale Up Quantum Computers, Award-Winning UChicago Research Finds

Jan 10, 2022
UChicago CS News

EPiQC Research Receives Best Paper Award at IEEE Quantum Week

Oct 22, 2021
UChicago CS News

UChicago and EPiQC Alum Yongshan Ding Joins Yale in Faculty Position

Oct 08, 2021
arrow-down-largearrow-left-largearrow-right-large-greyarrow-right-large-yellowarrow-right-largearrow-right-smallbutton-arrowclosedocumentfacebookfacet-arrow-down-whitefacet-arrow-downPage 1CheckedCheckedicon-apple-t5backgroundLayer 1icon-google-t5icon-office365-t5icon-outlook-t5backgroundLayer 1icon-outlookcom-t5backgroundLayer 1icon-yahoo-t5backgroundLayer 1internal-yellowinternalintranetlinkedinlinkoutpauseplaypresentationsearch-bluesearchshareslider-arrow-nextslider-arrow-prevtwittervideoyoutube