Compositional Higher-Order Model Checking: Logics, Models and Algorithms
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
The construction of bug-free programs is a challenging research problem of international importance and huge potential impact. Yet the traditional approaches to achieving confidence in software, such as testing and debugging, are not effective, often accounting for 50-75% of the total development cost.
In the past decade, automated verification techniques such as model checking have made great strides towards remedying this situation, especially when applied to first-order imperative programs such as C. Model checking is an approach to program verification that promises accurate analysis with pushdown automation. To model check a program against a correctness property, one first expresses the correctness property as a formula of a decidable logic. Then an abstract, typically finite, model of the system is constructed, which is then checked exhaustively for violation of the formula. Tools such as SLAM and Terminator demonstrate that model checking is scalable and highly effective for C-like programs.
This project is about the application of model checking and its allied automated verification methods to higher-order functional programs. Functional programs have long been applied to real-world tasks. Programmers use functional languages because they can build more robust code more quickly and with fewer errors then they could before, thereby boosting reliability and cutting costs. Others turn to functional languages because of the advantages they offer in data parallelism, concurrency, GPGPU and cloud programming. Examples: The Microsoft .NET language F# has emerged as a prototyping language of choice in finance and scientific applications. The concurrency-oriented functional language Erlang is a natural fit for programming multicore CPUs, networked servers, distributed databases, GUIs, and monitoring, control and testing tools. Thus by making functional programming safer and more robust and productive, techniques and tool support for the formal analysis of functional programs will bring significant benefits to the digital economy as a whole, but especially to financial modelling, scientific applications, computing and telecommunications, which are vital to current and future UK economic success.
Our GOAL is to develop a scalable, fully-automatic and well-founded method for the verification of functional programs, based on a compositional approach to Higher-Order Model Checking. Our approach is novel: we marry semantic methods (notably game semantics and intersection types) with algorithmic and automata-theoretic techniques from automated verification and program analysis. The verification problem is intrinsically challenging, not least because of its hyper-exponential worst-case complexity. Nevertheless a prototype implementation of our model checking algorithm, PREFACE, readily scales to recursion schemes of thousands of rules, well beyond the capabilities of current state-of-the-art higher-order model checkers, thus indicating that our approach is very promising. Hence our RESEARCH HYPOTHESIS: It is possible to design well-founded yet practical program verification procedures. This will be achieved by a principled approach based on COMPOSITIONAL Higher-Order Model Checking.
In the past decade, automated verification techniques such as model checking have made great strides towards remedying this situation, especially when applied to first-order imperative programs such as C. Model checking is an approach to program verification that promises accurate analysis with pushdown automation. To model check a program against a correctness property, one first expresses the correctness property as a formula of a decidable logic. Then an abstract, typically finite, model of the system is constructed, which is then checked exhaustively for violation of the formula. Tools such as SLAM and Terminator demonstrate that model checking is scalable and highly effective for C-like programs.
This project is about the application of model checking and its allied automated verification methods to higher-order functional programs. Functional programs have long been applied to real-world tasks. Programmers use functional languages because they can build more robust code more quickly and with fewer errors then they could before, thereby boosting reliability and cutting costs. Others turn to functional languages because of the advantages they offer in data parallelism, concurrency, GPGPU and cloud programming. Examples: The Microsoft .NET language F# has emerged as a prototyping language of choice in finance and scientific applications. The concurrency-oriented functional language Erlang is a natural fit for programming multicore CPUs, networked servers, distributed databases, GUIs, and monitoring, control and testing tools. Thus by making functional programming safer and more robust and productive, techniques and tool support for the formal analysis of functional programs will bring significant benefits to the digital economy as a whole, but especially to financial modelling, scientific applications, computing and telecommunications, which are vital to current and future UK economic success.
Our GOAL is to develop a scalable, fully-automatic and well-founded method for the verification of functional programs, based on a compositional approach to Higher-Order Model Checking. Our approach is novel: we marry semantic methods (notably game semantics and intersection types) with algorithmic and automata-theoretic techniques from automated verification and program analysis. The verification problem is intrinsically challenging, not least because of its hyper-exponential worst-case complexity. Nevertheless a prototype implementation of our model checking algorithm, PREFACE, readily scales to recursion schemes of thousands of rules, well beyond the capabilities of current state-of-the-art higher-order model checkers, thus indicating that our approach is very promising. Hence our RESEARCH HYPOTHESIS: It is possible to design well-founded yet practical program verification procedures. This will be achieved by a principled approach based on COMPOSITIONAL Higher-Order Model Checking.
Planned Impact
SCIENTIFIC COMMUNITY: KNOWLEDGE CREATION
This project will impact the scientific community because of the new knowledge that will be created. The proposed research contributes chiefly to three areas:
A. Verification and Correctness
B. Programming Languages
C. Theory of Computing, especially Logic and Algorithms, Game Semantics, and Lambda Calculus and Types
The work will impact on and benefit the academics and researchers working in these areas. The manner of the impact and the nature of the knowledge that will be created are explained in the section on Academic Beneficiaries.
Research areas A and B above are PRIORITY AREAS which EPSRC has earmarked for growth, thus underlining the national importance of the proposed work.
FINANCIAL MODELLING, SCIENTIFIC APPLICATIONS, COMPUTING AND TELECOMMUNICATIONS: SAFER AND MORE ROBUST CODE
In terms of the strategic themes identified by EPSRC, this proposal sits most naturally with the DIGITAL ECONOMY theme (in particular, with the CLOUD COMPUTING, and VALUE CREATION AND CAPTURE subthemes - see (ii) and (iii) below, respectively).
The construction of bug-free programs is a challenging research problem of international importance and huge potential impact. In a National Institute of Standards and Technology report of 2002, the cost to the US economy of faulty software was estimated at $60 billion. It is vitally important to transfer the benefits of model checking and other automatic verification techniques to higher-order functional languages such as F#, OCaml, Haskell and Erlang.
(i) Higher-order constructs such as first-class functions, lambda-expressions and closures are now basic features of the most widely-used languages such as Javascript, Perl5, Python, C# and C++0x, which are standard in web programming, hardware and embedded systems design.
(ii) Because functional languages support domain-specific languages and are good for organising data parallelism, they are widely used in scientific applications and financial modelling.
(iii) The absence of mutable variables and the use of monadic structuring principle to encapsulate side-effects make functional languages attractive for concurrent programming, which has become extremely important thanks to the rapid growth of multi-core and GPGPU processing and cloud computing.
Thus, by making functional programming safer and more robust and productive, techniques and tool support for the formal analysis of functional programs will bring significant benefits to financial modelling, scientific applications, and the computing and telecommunications industries, which are vital to current and future UK economic success.
WEALTH CREATION
The development of verification techniques and tools is an important precursor to wealth creation because of the opportunities for licensing and spin-offs. Indirectly all of society will benefit because they give rise to safe and reliable software. Our daily lives rely on software infrastructure for banking, communications, travel, shopping, and many other necessities. Ultimately better verification techniques and tools for software will lead to better quality of life in the digital world.
This project will impact the scientific community because of the new knowledge that will be created. The proposed research contributes chiefly to three areas:
A. Verification and Correctness
B. Programming Languages
C. Theory of Computing, especially Logic and Algorithms, Game Semantics, and Lambda Calculus and Types
The work will impact on and benefit the academics and researchers working in these areas. The manner of the impact and the nature of the knowledge that will be created are explained in the section on Academic Beneficiaries.
Research areas A and B above are PRIORITY AREAS which EPSRC has earmarked for growth, thus underlining the national importance of the proposed work.
FINANCIAL MODELLING, SCIENTIFIC APPLICATIONS, COMPUTING AND TELECOMMUNICATIONS: SAFER AND MORE ROBUST CODE
In terms of the strategic themes identified by EPSRC, this proposal sits most naturally with the DIGITAL ECONOMY theme (in particular, with the CLOUD COMPUTING, and VALUE CREATION AND CAPTURE subthemes - see (ii) and (iii) below, respectively).
The construction of bug-free programs is a challenging research problem of international importance and huge potential impact. In a National Institute of Standards and Technology report of 2002, the cost to the US economy of faulty software was estimated at $60 billion. It is vitally important to transfer the benefits of model checking and other automatic verification techniques to higher-order functional languages such as F#, OCaml, Haskell and Erlang.
(i) Higher-order constructs such as first-class functions, lambda-expressions and closures are now basic features of the most widely-used languages such as Javascript, Perl5, Python, C# and C++0x, which are standard in web programming, hardware and embedded systems design.
(ii) Because functional languages support domain-specific languages and are good for organising data parallelism, they are widely used in scientific applications and financial modelling.
(iii) The absence of mutable variables and the use of monadic structuring principle to encapsulate side-effects make functional languages attractive for concurrent programming, which has become extremely important thanks to the rapid growth of multi-core and GPGPU processing and cloud computing.
Thus, by making functional programming safer and more robust and productive, techniques and tool support for the formal analysis of functional programs will bring significant benefits to financial modelling, scientific applications, and the computing and telecommunications industries, which are vital to current and future UK economic success.
WEALTH CREATION
The development of verification techniques and tools is an important precursor to wealth creation because of the opportunities for licensing and spin-offs. Indirectly all of society will benefit because they give rise to safe and reliable software. Our daily lives rely on software infrastructure for banking, communications, travel, shopping, and many other necessities. Ultimately better verification techniques and tools for software will lead to better quality of life in the digital world.
People |
ORCID iD |
| Luke Ong (Principal Investigator) |
Publications
Broadbent C
(2021)
Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
in ACM Transactions on Computational Logic
Broadbent C
(2021)
Collapsible Pushdown Parity Games
in ACM Transactions on Computational Logic
Cathcart Burn T
(2017)
Higher-order constrained horn clauses for verification
in Proceedings of the ACM on Programming Languages
Cotton-Barratt C
(2019)
ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States
in ACM Transactions on Programming Languages and Systems
| Description | The goal of this project is to develop a compositional approach to the model checking of higher-type trees with binders i.e. Böhm trees. The 3-way Automata-Logic-Games equivalence is one of the most elegant and practically useful results in the theory and practice of verification, especially model checking. A key discovery of this project is a generalisation of this equi-expressivity result to languages of higher-type Böhm trees, which may be viewed as higher-order functions over trees. We equip Stirling's alternating dependency tree automata (ADTA) with an ?-regular winning condition, and show that they are equi-expressive with Kobayashi-Ong intersection types. We then introduce higher-type mu-calculus, which extends mu-calculus with predicates for detecting variables, and corresponding constructs for detecting ?-abstractions. We show that higher-type mu-calculus is equi-expressive with a subclass of intersection types (equivalently, ADTA) called parity permissive. Higher-order pushdown automata play a key algorithmic role in the model checking of higher-order programs. We show that the diagonal problem for higher-order pushdown automata (HOPDA), and hence the simultaneous unboundedness problem, is decidable. From recent work by Zetzsche this means that we can construct the downward closure of the set of words accepted by a given HOPDA. This also means we can construct the downward closure of the Parikh image of a HOPDA. Both of these consequences play an important role in verifying concurrent higher-order programs expressed as HOPDA or safe higher-order recursion schemes. The results have appeared in a POPL 2016 paper. Verification methods that are compositional typically rely on denotational models for their soundness proof. We have made a series of contributions to models of higher-order functional programming, clarifying the relationship between a number of quantitative models (including game semantics, relational models, and models arising from type systems), which provide the semantic foundations for compositional higher-order model checking: 1. We show that the following three interpretations of higher-order functional programs, namely, (i) as a collection of resource terms by the Taylor expansion, (ii) as a collection of plays by game semantics, and (iii) as a collection of types by a non-idempotent intersection type assignment system, are essentially the same. 2. We introduce a variant of the resource calculus, the rigid resource calculus, in which a permutation of elements in a bag is distinct from but isomorphic to the original bag. It is designed so that the Taylor expansion within it coincides with the interpretation by generalised species of Fiore et al., which generalises both Joyal's combinatorial species and Girard's normal functors, and which can be seen as a proof-relevant extension of the relational model. 3. Motivated by a tight connection between Joyal's combinatorial species and quantitative models of linear logic, we introduce weighted generalised species (or weighted profunctors), where weights are morphisms of a given symmetric monoidal closed category (SMCC). For each SMCC W, we show that the category of W-weighted profunctors is a Lafont category, a categorical model of linear logic with exponential. As a model of programming languages, our construction of gives a unified framework that induces adequate models of nondeterministic, probabilistic, algebraic and quantum programming languages by an appropriate choice of the weight SMCC. The above results have appeared in LICS 2016, LICS 2017 and LICS 2018 respectively. As a result of the work funded through this award, we have discovered a new approach to the automatic verification of higher-order programs that combines automated deduction and constraint solving, called Higher-order Constrained Horn Clauses. 1. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. This work has appeared in a paper at POPL 2018. 2. We have also advanced the logical and algorithmic foundations of higher-order constrained Horn clauses. We present a simple resolution proof system for higher-order constrained Horn clauses (HoCHC), and prove its soundness and refutational completeness with respect to both the standard and Henkin semantics. As corollaries, we obtain the compactness theorem and semi-decidability of HoCHC for semi-decidable background theories, and we prove that HoCHC satisfies a canonical model property. This work has appeared in a paper at LICS 2019. |
| Exploitation Route | Researchers in verification will find novel ingredients in our compositional method and semantic approach applicable to model checking in general; while those in game semantics and type theory will find that our algorithmic angle raises new questions and increases the applicability of their work. Users and developers of software model-checkers will likely find algorithms, optimisation techniques and tools arising from the project useful to their own work. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Education,Electronics,Other |
| URL | http://mjolnir.cs.ox.ac.uk/horus/ |
| Description | Croucher Foundation Scholarship (Carol Mak) |
| Amount | £80,000 (GBP) |
| Organisation | The Croucher Foundation |
| Sector | Charity/Non Profit |
| Country | Hong Kong |
| Start | 10/2017 |
| End | 03/2021 |
| Description | Differentiable Probabilistic Programming Semantics. Probability and Programming Research Award, Facebook Research |
| Amount | £80,000 (GBP) |
| Organisation | |
| Sector | Private |
| Country | United States |
| Start | 05/2019 |
| End | 04/2021 |
| Description | EPSRC DTP Studentship (Andrew Kenyon-Roberts) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2019 |
| End | 03/2023 |
| Description | EPSRC DTP Studentship (Dominik Wagner) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2018 |
| End | 03/2022 |
| Description | EPSRC DTP Studentship (Fabian Zaiser) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2019 |
| End | 03/2023 |
| Description | EPSRC DTP Studentship (Mario Alvarez-Picallo) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2015 |
| End | 03/2019 |
| Description | EPSRC DTP Studentship (Rolf Morel) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2018 |
| End | 03/2022 |
| Description | EPSRC DTP Studentship (Toby Cathcart Burn) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2017 |
| End | 03/2021 |
| Description | EPSRC DTP Studentship (Tom Mattinson) |
| Amount | £80,000 (GBP) |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 10/2017 |
| End | 03/2021 |
| Description | National Cyber Security Centre, Research Institute in Verified Trustworthy Software Systems (VeTSS): Higher-order Program Invariants and Higher-order Constrained Horn Clauses |
| Amount | £82,100 (GBP) |
| Organisation | The Research Institute on Verified Trustworthy Software Systems |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 10/2019 |
| End | 03/2023 |
| Description | Research Programme on Logic, Automata and Games, Institute for Mathematical Sciences, National University of Singapore, 22 August - 23 September 2016 |
| Amount | $180,000 (SGD) |
| Organisation | National University of Singapore |
| Sector | Academic/University |
| Country | Singapore |
| Start | 08/2016 |
| End | 09/2016 |
| Description | Scatcherd Scholarship (Jerome Jochems) |
| Amount | £80,000 (GBP) |
| Organisation | University of Oxford |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 10/2015 |
| End | 04/2019 |
| Title | ASTNAR: Almost sure termination of non-affine recursive functional programs |
| Description | The theoretical results presented in the PLDI 2021 paper by Beutner and Ong give a sound (but incomplete) method for proving a program to be almost surely terminating (AST). This tool implements the algorithm extracted from the soundness proof. The goal is to verify a fixpoint abstraction to be AST on every possible input. The only argument passed to our tool is therefore the fixpoint term in question. The tool analyses the term by counting the number of recursive calls along each branch and computes the probability of individual branches by computing the volume of a convex polytope using the external tool vinci. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2021 |
| Provided To Others? | Yes |
| Impact | This is the first tool that can prove almost sure termination of non-affine recursive functional programs with continuous distributions. |
| URL | https://drive.google.com/drive/folders/1sFpIqPuVyoA6uobVWEm55w-FzMo-BrRZ?usp=sharing |
| Title | Constraint Solver for the theory of trees |
| Description | The first-order theory of finite and infinite trees has been studied since the eighties, especially by the logic programming community. Following Djelloul, Dao and Fruhwirth, extend this theory with an additional predicate for finiteness of trees, which is useful for expressing properties about (not just datatypes but also) codatatypes. Based on their work, we present a simplification procedure that determines whether any given (not necessarily closed) formula is satisfiable, returning a simplified formula which enables one to read off all possible models. Our extension makes the algorithm usable for algebraic (co)datatypes, which was impossible in their original work due to restrictive assumptions. We also provide a prototype implementation of our simplification procedure and evaluate it on instances from the SMT-LIB. Our implementation can be found at https://github.com/fzaiser/tree-theory-solver/. Additionally, there is a web interface at http://mjolnir.cs.ox.ac.uk/trees-codata/. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2019 |
| Provided To Others? | Yes |
| Impact | To our knowledge, this is the first implemented constraint solver for the theory of trees that has a finiteness predicate, and can express properties about datatypes and codatatypes. |
| URL | http://mjolnir.cs.ox.ac.uk/trees-codata/index.php |
| Title | DefMono |
| Description | DefMono is a method for solving Higher-order Constrained Horn Clauses (HoCHC) by defunctionalisation. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2018 |
| Provided To Others? | Yes |
| Impact | DefMono is the first sound and complete solution method for HoCHC. |
| URL | http://mjolnir.cs.ox.ac.uk/dfhochc/ |
| Title | HORUS |
| Description | HORUS is tool implementation of a method for solving Higher-order Constrained Horn Clauses (HoCHC) that is based on refinement types. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2018 |
| Provided To Others? | Yes |
| Impact | Sound but incomplete, this is the first solution method for HoCHC. |
| URL | http://mjolnir.cs.ox.ac.uk/horus/ |
| Title | Lower bounds on termination probability of functional programs with continuous distributions |
| Description | This tool uses an interval-based approach to incrementally analyse the termination probability of arbitrary terms via a combination of stochastic symbolic execution and interval splitting. As this task is undecidable (even \Pi_0^2-complete) we cannot compute the exact probability of termination. Instead the tool gives lower bounds by stopping the computation at a user defined point. This can be specified by timeout or a recursion depth. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2021 |
| Provided To Others? | Yes |
| Impact | This is the first tool that can compute lower bounds of termination probabilities of functional programs with continuous distributions. |
| URL | https://drive.google.com/drive/folders/1sFpIqPuVyoA6uobVWEm55w-FzMo-BrRZ?usp=sharing |
| Description | Relating game semantics, intersection types and Taylor expansion of lambda terms |
| Organisation | University of Tokyo |
| Department | Department of Electrical Engineering and Information Systems |
| Country | Japan |
| Sector | Academic/University |
| PI Contribution | A program is interpreted as a collection of resource terms by the Taylor expansion, as a collection of plays by game semantics, and as a collection of types by a non-idempotent intersection type assignment system. This paper investigates the connection between these models and aims to show that they are essentially the same in a certain sense. Technically we study the relational interpretations of resource terms and of plays, which can be seen as non- idempotent intersection type assignment systems for resource terms and plays, respectively.We show that both relational interpretations are injective, have the same image, and respect composition. This result allows us to study a property of the game model by using the syntax of a resource calculus and vice versa. Categories |
| Collaborator Contribution | Professor Takeshi Tsukada contributed ideas and helped to write up the work for publication. |
| Impact | This has led to the publication of the following paper: Takeshi Tsukada, C.-H. Luke Ong: Plays as Resource Terms via Non-idempotent Intersection Types. LICS 2016: 237-246 |
| Start Year | 2016 |
| Description | VeTSS funded PhD Studentship "Higher-order Program Invariants and Higher-order Constrained Horn Clauses" |
| Organisation | University of Bristol |
| Department | Department of Computer Science |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | This is a collaborative project funded by VeTSS (Research Institute in Verified Trustworthy Software Systems, Imperial College, London), led by Luke Ong (University of Oxford) and Steven Ramsay (Bristol University). The goal of this studentship is to develop a unifying theory of higher-order program invariants, which can express the common, logical underpinnings of the subject and yet supports effective and reusable automated reasoning tools. |
| Collaborator Contribution | A first major contribution concerns the pattern-match safety problem, which is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. In a POPL2021 paper, Steven Ramsay and the project student, Eddie Jones, have presente a refinement type system that can be used to solve this problem. The system extends ML-style type systems with algebraic datatypes by a limited form of structural subtyping and environment-level intersection. A fully automatic, sound and complete type inference procedure for this system has been developed, which, under reasonable assumptions, is worst-case linear-time in the program size. Compositionality is essential to obtaining this complexity guarantee. A prototype implementation for Haskell is able to analyse a selection of packages from the Hackage database in a few hundred milliseconds. |
| Impact | Eddie Jones, Steven J. Ramsay: Intensional datatype refinement: with application to scalable verification of pattern-match safety. Proc. ACM Program. Lang. 5(POPL): 1-29 (2021) |
| Start Year | 2019 |