Language-Integrated Verification - DLS Talk by Ranjit Jhala (UCSD)

Date: 
Thursday, February 14, 2019 | 3:30pm - 5:00pm
Location: 
Hugh Dempster 110 (6245 Agronomy Rd)

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 continously 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: TBA


Find more undergrad events on our internal portal at https://my.cs.ubc.ca.

This event's address: https://my.cs.ubc.ca/event/2019/02/dls-talk-ranjit-jhala-ucsd

a place of mind, The University of British Columbia

 

ICICS/CS Building 201-2366 Main Mall
Vancouver, B.C. V6T 1Z4 Canada
Tel: 604-822-3061 | Fax: 604-822-5485
General: help@cs.ubc.ca
Undergrad program: undergrad-info@cs.ubc.ca
Graduate program: grad-info@cs.ubc.ca

Emergency Procedures | Accessibility | Contact UBC | © Copyright The University of British Columbia