Traditional software verification algorithms work by using a
combination of Floyd-Hoare Logics, Model Checking and Abstract Interpretation,
to check and infer suitable program invariants. However, these
techniques are problematic in the presence of complex but ubiquitous
constructs like generic data structures, first-class functions. We observe
that modern type systems are capable of the kind of analysis needed
to analyze the above constructs, and we use this observation to develop
Liquid Types, a new static verification technique which combines the
complementary strengths of Floyd-Hoare logics, Model Checking, and
Types. As a result, we demonstrate how liquid types can be used to
statically verify properties ranging from memory safety to data structure
correctness, in higher-order languages like ML. This presentation is
based on joint work with Patrick Rondon and Ming Kawaguchi.
This book constitutes the refereed proceedings of the 9th Asian Symposium on Programming Languages and Systems, APLAS 2011, held in Kenting, Taiwan, in December 2011. The 22 revised full papers presented together with 4 invited talks and one system and tool presentations were carefully reviewed and selected from 64 submissions. The papers are organized in topical sections on program analysis; functional programming; compiler; concurrency; semantics; as well as certification and logic.