Verifying Properties of the ML Family of Languages

The development of techniques for the computer-aided verification of finite-state systems such as digital hardware and communication protocols has been a great success story in computer science. Despite considerable progress over the past decade, the transfer of these techniques to software verification remains a challenging research problem. There are two main reasons: First, programs are potentially infinite-state systems, but verification tools of industrial scale are essentially finite-state technologies. Secondly modern programs - in which higher-order features, complex memory operations, non-local control flow, etc. are key features - can only be accurately modelled using highly-structured mathematical models, as studied in semantics. Unfortunately these models (with the exception of game models) have tended to be too "abstract" for algorithmic analysis.

Our goal is to develop verification techniques for higher-order (call-by-value) procedural languages with reference type, as exemplified by Ocaml, F# and other members of the ML family of programming languages. A task is to derive of algorithms for deciding observational equivalence (of an appropriate fragment of Reduced ML) by reduction to the equivalence of visibly pushdown automata, and to build a prototype implementation of it. Another task is to develop a notion of reachability test for higher-order procedural languages, and identify language fragments for which it is decidable and determine its complexity.