My academic interests (broadly) include:

• foundations of concurrency,
• process calculi,
• logic,
• model checking,
• software engineering and formal methods,
• distributed and parallel computing,
• performance modelling,
• computational systems biology,
• functional and concurrent programming languages,
• and any interesting applications thereof.

Ph.D.

My research is concerned with the development of a temporal logic and model checking algorithms for the continuous π-calculus. My supervisor is Ian Stark and my work continues the work of Marek Kwiatkowski.

The continuous π-calculus (cπ) is a process algebra with a compositional, continuous time and continuous space semantics in terms of real vector spaces. The ability to model a continuous state-space of real values is especially useful in the modelling of biochemical systems where the state of the system is described in terms of the real valued concentrations of chemical species. The project aims to augment the existing cπ theory with a means to perform model checking on cπ models. That is, the mechanical verification that some formal logical assertion holds for the model. A logic equipped with a notion of real numbers will need to be developed, suitable for making assertions about a continuous state space along with an algorithm for verification of these assertions.

I am developing a logic - which can be seen as a formal query langauge - for expressing behavioural properties of cπ models. The logic of behvaiour in context (LBC) is a time bounded temporal logic extended with a modality which allows things (i.e. new chemical species) to be introduced to the model. This allows the expression of properties of the behaviour when species are introduced to the model over time.

Some of this is described in more detail (with pictures) on this poster

M.Sc.

My M.Sc. thesis was on model checking the independence-friendly modal μ-calculus. Independence-friendly logic is an extension of first order logic which allows the expression of independence between quantifiers. IF logic potentially has applications in the verification of concurrent computer systems. However, even the smallest examples are so complex that they are almost impossible to do by hand. My project centred on the implementation of a model checker which checked models of concurrent systems (in CCS) against specifications expressed in a version of the modal μ-calculus which has been extended to express IF modalities. My M.Sc. supervisor was Julian Bradfield. See his research page for more information on IF logic and the modal μ-calculus.

Publications

• Clark A., Gilmore S., Georgoulas A., Hillston J., Stark I., Banks C., and Milios D. "Stochastic Modelling of the Kai-based Circadian Clock." (To appear) In Proceedings of Practical Applications of Stochastic Modelling, 2012
• Smithies A. and Banks C., "Developing a Social Collaborative Platform for a Curriculum Review Process: a Case Study of an Iterative Component Based Method." Proceedings of the 8th European Conference on e-Learning, p532, October 2009.

Talks

• May 2013: Modelling a posttranslational biochemical oscillator - A talk for PEPA Club detailing some of the results of modelling an ideal oscillator in cπ.
• September 2012: A logic of behaviour in context - A short talk introducing LBC given at the MLQA workshop.
• July 2012: A logic of behaviour in context and the continuous π-calculus - a talk introducing cπ and LBC, given for the CONTRAINTES group at INRIA, Paris.
• April 2012: Towards a logic of biochemical processes - a high level talk about my logic for continuous state spaces with guarantee, given to BCTCS 2012.
• October 2011: Continuous state-space model checking - a talk discussing my thesis proposal and recent work given to PEPA Club.
• February 2011: Temporal Logic for Systems Biology - a survey talk given to PEPA Club.

Teaching

• 2012/13: Teaching assistant for the Inf1-FP first year undergraduate functional programming course. As previous year, but teaching assitant as well as tutoring. I was in charge of setting Haskell based tutorial exercises and the auto-marking tools for automarking the examination. I also judged the programming competition and maintained the web pages.
• 2011/12: Tutor for the Inf1-FP first year undergraduate functional programming course. Students learn functional programming concepts and the Haskell functional programming language.
• 2010/11: Tutor for the System Design Project a third year undergraduate course in Informatics. The course consisted of a large group project to design, build, and program a football playing robot. Students were assessed by means of reports and demonstrations at significant milestones throughout the course and by a final tournament with academic and industry judges.