[Pl-seminar] Semantics Seminar Schedule

[Pete Manolios]

Ranjit is interested in meeting with faculty and students in PRL. If
anyone is interested in meeting with him, send me email. Ranjit is
available this Wednesday starting at 8:30 AM until 11:30 AM. If you're
interested, let me know what your availability is and what your
preferred meeting times are.

Cheers,
Pete

On Mon, Feb 9, 2009 at 12:05 AM, Mitchell Wand <wand at ccs.neu.edu> wrote:
> 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
>
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar
>



-- 
Pete Manolios
Northeastern University
http://www.ccs.neu.edu/home/pete