This page presents some of my research interests. If you are interested in my publications, please go to the publications page.
My research interests are generally in mathematical approaches to software quality. More specifically:
- Calculation of algorithms from their formal specification
- Algorithm design
- Formal verification of programs
- Functional programming
I am also interested in:
- Teaching of mathematics
- Parallel programming
I am a member of the project Inference Mechanisms for a Separation and Numerical Domain (EPSRC Funded Project EP/G042322), where I conduct research on automated verification of heap-manipulating programs using separation logic. Currently, I am working on the verification of FreeRTOS, a real-time, multitasking, preemptive operating system for embedded devices.
In 2010, I finished my PhD on principles and foundations of algorithmic problem solving (PhD thesis). The goal of my thesis is to articulate principles and techniques that can be used to solve algorithmic problems more effectively. I have also developed educational material supporting the use of an algorithmic and calculational approach to number theory, including new algorithms and results.
See also the page on Algorithmic Problem Solving.
Parallel Programming in Java
I was a member of the PPC-VM project, whose goal was to provide an “intelligent” parallel virtual machine capable of automatically manage a set of computing nodes and effectively distributing tasks among them. My contributions to the project were:
- creation of a tool that transforms Java programs into programs that are able to distribute themselves automatically among a set of computing nodes;
- development of JaSkel, a framework providing parallel skeletons to write parallel programs; this work was presented at CCGrid ’06;
- development and testing of ParC#, a parallel computing platform developed on top of the Mono project; this work was presented at PaCT ’05.
Formal Specification Systems
I have contributed to the Camila project, by exploring how concepts from the VDM specification language and the functional programming language Haskell can be combined. My contribution includes experiments in expressing VDM’s data types (e.g. maps, sets, sequences), data type invariants and pre-conditions, within the Haskell language. This work was presented at the Overture Workshop, Newcastle (UK), 2005.