# Verifying Properties of the ML Family of Languages

1st October 2008 to 30th September 2011

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.

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.