[Colloquium] TTI-C Talk: Ranjit Jhala, UC San Diego

[Julia MacGlashan]

When:              TODAY: Thursday, October 16 @ 10:30am

 

Where:            ROOM CHANGE: TTI-C Lobby Conference Room #201

 

Who:                Ranjit Jhala, University of California, San Diego

 

Topic:              Liquid Types

 

 

ABSTRACT:  We present Logically Qualified Data Types, abbreviated to Liquid
Types, a new static verification technique which combines the complementary
strengths of automated deduction (SMT solvers), model checking (Predicate
Abstraction), and type systems (Hindley-Milner inference). Liquid Types
automate static verification of deep invariants by combining local
implication checks over simple refinement predicates with global subtyping
checks. The former are discharged using SMT solvers, and the latter using
standard type-based mechanisms. We have implemented Liquid Types in a tool
Dsolve, which takes as input an Ocaml program and a set of logical
qualifiers and infers liquid types for the expressions in the program. To
demonstrate the utility of our approach, we describe experiments using
Dsolve to statically verify, with minimal annotations, the safety of array
accesses on a diverse set of benchmarks, and the key invariants of a variety
of data structure libraries including several sorting implementations, AVL
trees, red-black trees, finite, balanced binary search maps, and an
extensible vector library.

 

(Joint work with Patrick Rondon and Ming Kawaguchi)

 

BIO:  Ranjit Jhala is an Assistant Professor in the Department of Computer
Science and Engineering at UC San Diego. Before joining UCSD, he was a
graduate student at UC Berkeley. Ranjit is interested in Programming
Languages and Software Engineering, more specifically, in techniques for
building reliable computer systems. His work draws from, combines and
contributes to methods the areas of Model Checking, Program Analysis and
Automated Deduction.

 

Contact:          Amal Ahmed, TTI-C         amal at tti-c.org
834-6832

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20081016/431403f9/attachment.htm