Grants

Related Grants

The grant is used to pump prime new activities, resulting in the development of new grants, or to support existing grants. The following projects have strong associations with the platform grant:

Current Grants

• App Guarden

• COINVENT

• Computational Creativity Theory

• Computer-based Modelling for Safe Intra-hospital Patient Transfers

• Creative Code Generation for Interactive Media

• DTacs - Program Verifier Tactics: Reducing the Development Time for Program Verifiers with re-usable Verification Strategies

• Essence

• EPSRC Centre for Doctoral Training in Intelligent Games & Game Intelligence (IGGI)

• EPSRC Centre for Doctoral Training in Pervasive Parallelism

• A flexible and adaptable proof tool for verification of control systems in evolving markets (partly funded by IAA and platform grant; joint with D-RisQ)

• Programmable embedded platforms for remote and compute intensive image processing applications

• ProofPeer

• Robustness-as-evolvability: building a dynamic control plane with Software-Defined Networking

• The development of rigorous methods for the design of complex systems, in line with Military and Civil standards for complex hardware and software (EPSRC Industrial Case grant EP/J501992)

• SICSA Industrial Fellowship (Gudmund Grov working with D-RisQ)

• WHIM

Completed Grants

• AI4FM: the use of AI to aid automation of proof search in Formal Methods

• Automatic Proof Procedures for Polynomials and Special Functions

• UCT for Games and Beyond

Flexibility Funding

A key ingredient in the creation of new grants, or to bridge and complete existing work, is the flexibility funding. These are short term projects (typically 2-6 months), and the small grants have been funded:

• Invariant and Code Synthesis via Structure Manipulation (RA: Ewen Maclean)

  • Exploratory Study into the Debugging of Automatically Constructed Ontologies (RA: Andriana Evgenia Gkaniatsou)

  • Generating English Descriptions of IsaPlanner Proofs (RA: Daniel Raggi)

  • A Cloud-Based Interactive Theorem Proving System With a Focus On (Applied) Mathematics (RA: Steven Obua)

  • A Diagrammatic Tool for Formally Verifying Web Service Composition (RA: Sean Wilson)

  • Proof-failure Driven Theory Formation for Formal Methods (RA: Teresa Llano)

  • Theory and Proof Script Refactoring (RA: Dominik Dietrich)

  • Theory Formation for Video Game Analytics (RA: Jeremy Gow)

  • A Diagrammatic Tool for Formally Verifying Web Service Composition and Health Care Work Flows (RA: Sean Wilson & Petros Papapanagiotou)

  • A Guesstimation Web Service (RA: Gintautas Sasnauskas)

  • Automated Theory Formation over Social Network data (RA: Ramin Ramezani)

  • Automated Lemma Discovery (ACL2 meets HR) (RA: Teresa Llano)

  • Hierarchical Proof Exploration in HOL Light and Proof General (RA: Steven Obua)

  • Interactive hypothesis generator (RA: Michael Chan)

  • Investigating the impact of application frameworks for analysing Java applications (RA: Aziem Chawdhary)

  • SuperStrategy: SuperTac in the Strategy Language (RA: Yuhui Lin)

  • A mapping between ServiceComposer and SCOlog for Health Care Workflows (RA: Areti Manataki)

  • Humatic - the Box Calculas Going Live! (RA: Kos Devyatov)

  • Machine assisted mathematical discovery (RA: Roy McCasland)

  • Massively Collaborative Theorem Proving/Hierarchical Proofs in HOL Light (RA: Steven Obua)

  • Learning Domain-Specific Guidance for Theory Generation (RA: Jeremy Gow)

  • JAR Paper on Reformation (RA: Boris Mitrovic)

  • Turning SPARK VCs into Pictures (RA: Madiha Jami)

  • MIL for tactic learning (RA: Colin Farquhar)

  • GUI for PSGraph (RA: Pierre Le Bras)

  • Tooling on the EDGE (RA: Peter Kovacs)

  • Evaluation of the CHAIn System (RA: Diane Bental)

  • Security and reasoning: research project scoping and writing (RA: Bob Atkey)

  • Some CoInventing ProofPower work (Consultant: Rob Arthan)

  • Secondment to D-RisQ; partly funded by an IAA (RA: Yuhui Lin)

  • An AI4FM book (RA: Iain Whiteside)

  • Informing design and safety analysis via novel combinations of automated reasoning techniques (RA: Rajiv Murali)

  • Elegance (RA: Joe Davidson)

  • The application of Reformation to Repair Faulty Analogical Blends (RA: Aristeidis Tsalos)

  • Theorem Recommendations via Smart Clustering (RA: Sebastian Schulze)

  • GUI for PSGraph - part 2 (RA: Pierre Le Bras)

  • A Tacny Demonstration (RA: Tumas Vytautas)

  • Integrating Rodin and PSGraph (RA: Yibo Liang)

  • Extending the CHAIn system and extending its application within the e-response domain (RA: Gábor Bella)