Driven by the increasing power of automated theorem provers and
recent high-profile software failures,
fully automated program verification has seen a surge of interest
in recent years [1]}, [2]}, [3]}, [4]}, [5]}, [6]}.
In particular, refinement types
[7]}, [8]}, [9]}, [10]},
which refine base types with logical predicates, have been shown to be a practical
approach for program verification that are amenable to
(sometimes full) automation [11]}, [12]}, [13]}, [14]}.
Despite promising advances [15]}, [16]}, [17]},
the sound and precise application of refinement types (and program
verification in general) in settings with mutability and aliasing
(e.g., Java, Ruby, etc.) remains difficult.
<FIGURE>