| EPSRC Reference: |
EP/M023974/1 |
| Title: |
Compositional Higher-Order Model Checking: Logics, Models and Algorithms |
| Principal Investigator: |
Ong, Professor CHL |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
Standard Research |
| Starts: |
01 July 2015 |
Ends: |
31 May 2020 |
Value (£): |
630,834
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
05 Mar 2015
|
EPSRC ICT Prioritisation Panel - Mar 2015
|
Announced
|
|
|
Summary on Grant Application Form |
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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |