Research
Research projects
This project will introduce more certainty into the selection of cloud services through the introduction of a smart and continuously adaptive cloud broker. The broker will act as an intermediary between end users and cloud service providers in order to enhance service delivery and service value. This brokerage service will be designed to manage heterogeneous cloud offerings, including public, private or hybrid environments. Such brokerage will open up an entirely new multi-cloud marketplace, allowing applications to be simply deployed to the optimal provider and resource type, reducing complexity, vendor lock-in and computational running costs
This project aims to formalise safety and security proprieties of software-defined networking (SDN). We are, in particular, interested in designing a formal framework which is able to reason about a SDN formalisation with respect to attacks and network resources.
State of the art program verifiers are often classified as auto-active: they rely on powerful SMT solvers to discharge proof obligations, and when they fail, the user will guide the proof in the program text through annotations. The Tacny project aims to develop a language within the Dafny program verifier to allow users to encode reusable proof strategies. Potential advantages include: reuse of verification patterns, meaning improved automation and reduced development time; reduction of annotation overhead, i.e. the code to annotation factor is reduced; and more readable program text as low-level proof guidance can be hidden in the tactics.
We are interested in developing a graphical language for proof strategies (PSGraph language). The Tinker tool, which is the first implementation of PSGraphs. It adopts a generic theorem prover independent framework. We have currently connected it to both Isabelle and ProofPower. I was a member of the Tinker development team, providing an implementation of the PSGraph language. Here, I developed the underlying core and GUI, and integrated the language with new theorem provers.
Proof Obligation Proofs Patched Automatically (POPPA)
This is my PhD research. This work is part of the EPSRC funded AI4FM project. It aimed to improve the proof automation for formal methods using a high-level proof-planning theorem proving techniques, i.e. rippling. I targeted at one family of proofs from one popular formal methods, called Even-B invariant proofs. I was, in particular, interested in the case when proofs, and then we developed proof patches based on the high-level guidance for rippling to discover missing lemmas, apply a case split or unfold definitions.