...
Liquid
...
Types:
...
SMT
...
Solver-based
...
Types
...
We
...
describe
...
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
...
show
...
how
...
in
...
a
...
high-level
...
functional
...
setting
...
(e.g.
...
Ocaml),
...
liquid
...
types
...
can
...
be
...
used
...
to
...
statically
...
verify
...
a
...
variety
...
of
...
invariants
...
like
...
array-bound-safety,
...
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.
...
If
...
time
...
permits,
...
we
...
will
...
briefly
...
describe
...
how
...
liquid
...
types
...
can
...
be
...
applied
...
to
...
a
...
low-level
...
imperative
...
setting
...
(e.g.
...
C).
...
Ranjit Jhala, University of California, San Diego, USA
Ranjit Jhala is an Associate Professor in the Department of Computer Science and Engineering at UC San Diego. He is interested in applying techniques from Programming Languages and Software Engineering to solve computing problems, in particular, to build reliable computer systems. His work draws from, combines and contributes to methods the areas of Model Checking, Program Analysis, Type Systems and Automated
Deduction. Presently, he is madly in love with typeclasses.
| Attachments | ||
|---|---|---|
|