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

Students posing at competition

UChicago Undergrad Team Places Second Overall In Regionals For World’s Largest Programming Competition

Mar 17, 2023
Garcia sitting in a jet engine

Student Spotlight: Gabi Garcia’s Bridge Between CS and Classics

Jan 30, 2023

Assistant Professor Robert Rand Receives Air Force Young Investigator Grant

Dec 19, 2022
Haifeng Xu

New CS and DSI Faculty Haifeng Xu Brings Strategic Intelligence to NeurIPS 2022

Nov 28, 2022

UChicago’s Parsl Project Pivots to Sustainability and Community with New Grants

Nov 17, 2022

UChicago CS Research Finds New Angle on Database Query Processing with Geometry

Nov 08, 2022

Civic Tech Pioneer James Turk Joins UChicago CS to Teach in MPCS, CAPP

Oct 06, 2022

Asst. Prof. Aloni Cohen Receives Award For Revealing Flaws in Deidentifying Data

Sep 09, 2022

UChicago/Argonne Computer Scientist Ian Foster Receives ACM/IEEE Ken Kennedy Award

Sep 07, 2022

UChicago Hosts NSF Workshop on Frontiers of Quantum Advantage

Aug 15, 2022

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

Aug 11, 2022

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

Aug 09, 2022
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