[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, February 11, 2009
(* I THINK I'VE GOT THE DATE RIGHT NOW...  *)
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Ranjit Jhala
University of California, San Diego

Liquid Types

We present Logically Qualified Data Types, abbreviated to Liquid
Types, a new static program verification technique which combines the
complementary strengths of automated deduction (SMT solvers), model
checking (Predicate Abstraction), and type systems (Hindley-Milner
inference).  We have implemented the technique in a tool that infers
liquid types for Ocaml programs.  To demonstrate the utility of our
approach, we show how liquid types reduce, by more than an order of
magnitude, the manual annotations required to statically verify (1)
the safety of array accesses on a diverse set of benchmarks, and (2)
invariants like sortedness, balancedness, binary-search-ordering,
variable ordering, set-implementation, heap-implementation, and
acyclicity of data structure libraries for list-sorting, union-find,
splay trees, AVL trees, red-black trees, heaps, associative maps,
extensible vectors, and binary decision diagrams.  (Joint work with
Patrick Rondon and Ming Kawaguchi)

 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.

Host: Pete Manolios

================================================================

Upcoming Events:

# 2/18 Adam Chlipala, Liberating Semi-Automated PL Proofs from Binder
Bookkeeping 

Wouldn't you like to give a talk?

--Mitch