<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class=""><div dir="auto" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div apple-content-edited="true" class="" style="orphans: 2; widows: 2;"><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div class="" style="margin: 0in 0in 0.0001pt;"><span class=""><font face="Cambria" size="4" class=""></font></span></div><div class="" style="margin: 0in 0in 0.0001pt;"><span class=""><font face="Cambria" size="4" class=""><br class=""></font></span></div><div class="" style="margin: 0in 0in 0.0001pt;"><span class=""><span class=""><b class=""><font class="" face="Cambria" size="4">Tuesday, January 22, 2019 at 2:30 pm</font></b></span></span></div><div class="" style="margin: 0in 0in 0.0001pt;"><b class=""><font class="" face="Cambria" size="4">JCL 390</font></b></div><div class="" style="margin: 0in 0in 0.0001pt;"><font face="Cambria" size="4" class=""><span class=""><span class=""><b class=""><br class=""></b></span><br class=""><font class=""><b class=""><font class="">Title:</font></b><span class=""> </span></font></span><b class=""><font class="">Language-Integrated Verification</font></b></font></div></div></div></div><font class="" face="Cambria" size="4" style="orphans: 2; widows: 2;"><br class=""></font><div class="" style="orphans: 2; widows: 2;"><b class=""><font class="" face="Cambria" size="4">Abstract:</font></b></div><div class="" style="orphans: 2; widows: 2;"><font class="" face="Cambria" size="4">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).<br class=""> <br class="">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.<br class=""> <br class="">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.</font></div><div class="" style="orphans: 2; widows: 2;"><span class=""><font face="Cambria" size="4" class=""><br class=""></font></span></div><div class="" style="orphans: 2; widows: 2;"><br class=""></div><div class="" style="orphans: 2; widows: 2;"><span class=""><b class=""><i class=""><font face="Cambria" size="4" class="">Bio:</font></i></b></span></div><div class="" style="orphans: 2; widows: 2;"><i class=""><font face="Cambria" size="4" class="">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.</font></i></div><div class="" style="orphans: 2; widows: 2;"><span class=""><font face="Cambria" size="4" class=""><br class=""><font class="">Host: Ravi Chugh</font></font></span></div></div><font face="Cambria" size="4" class=""><br class="Apple-interchange-newline"><br class="Apple-interchange-newline"></font></div><div class=""><font face="Cambria" size="4" class=""><br class="webkit-block-placeholder"></font></div><div class=""><font face="Cambria" size="4" class="">PDF:</font></div><div class=""></div></div></body></html>