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

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)