[Pl-seminar] OOPS^2!!

Mitchell Wand wand at ccs.neu.edu
Tue Feb 3 12:19:55 EST 2009


OK,  not only is the talk not on January whatever, but it's also not
tomorrow.

The talk is in fact scheduled for *next* week, 2/11.

Sorry for the all the confusion.

--Mitch


On Tue, Feb 3, 2009 at 10:53 AM, Mitchell Wand <wand at ccs.neu.edu> wrote:

> NU Programming Languages Seminar
> **OOPS, THIS TIME LET'S GET THE DATE RIGHT**
> Wednesday, February 4, 2009
> 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/11 Adam Chlipala, Mechanized Semantics with Definitional Compilers
>
> Wouldn't you like to give a talk?
>
> --Mitch
>
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar
>
>
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the pl-seminar mailing list