My interests lie broadly in process algebras, particularly CSP, and in protocol security.
My current research on process algebras is focussed on CSP. In particular, I am the lead developer of the FDR3 model checker, which is a verifier for CSP. FDR3 is an extremely capable model checker that is able to efficiently verify systems that consist of tens of billions of states. Further, it has a very expressive input language in the form of machine-CSP, thus allowing very complex systems to be modelled.
My current security research concerns the verification of layered security protocols. During my doctorate, I extended the high-level strand spaces model to allow arbitrary stacks of protocols to be verified by abstraction. Currently I am interested in extending these results in various ways, in addition to considering how the correctness proofs, which must currently be done by hand, can be automated.
CPA 2014: I am the local organiser for this year's Communicating Process Architectures conference: please do consider submitting a paper and/or attending. More details are available here.
Thomas Gibson-Robinson is a Junior Research Fellow at University College. He completed his doctorate under the supervision of Gavin Lowe at Oxford. He previously received his MCompSci in 2010 from Oxford.
FDR3: a parallel refinement checker for CSP
Thomas Gibson−Robinson‚ Philip Armstrong‚ Alexandre Boulgakov and A.W. Roscoe
In International Journal on Software Tools for Technology Transfer. 2015.
Computing Maximal Bisimulations
Alexandre Boulgakov‚ Thomas Gibson−Robinson and A.W. Roscoe
In Formal Methods and Software Engineering − 16th International Conference on Formal Engineering Methods‚ ICFEM 2014‚ Proceedings. 2014.
FDR into The Cloud
Thomas Gibson−Robinson and A.W. Roscoe
In Communicating Process Architectures. 2014.