Thomas Gibson-Robinson

Thomas Gibson-Robinson

Senior Researcher

Junior Research Fellow, University College

Leaving date: 30th June 2019

Themes:

• Automated Verification

See Also:

• FDR4

Interests

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.

Biography

Thomas Gibson-Robinson is a Senior Researcher in the Department of Computer Science. Previously he was a Junior Research Fellow at University College, having completed his doctorate under the supervision of Gavin Lowe at Oxford. He previously received his MCompSci in 2010 from Oxford.

Selected Publications

View AllManage publications

• 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.

  Details about FDR3: a parallel refinement checker for CSP | BibTeX data for FDR3: a parallel refinement checker for CSP | DOI (10.1007/s10009-015-0377-y) | Link to FDR3: a parallel refinement checker for CSP

• 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.

  Details about Computing Maximal Bisimulations | BibTeX data for Computing Maximal Bisimulations | DOI (10.1007/978-3-319-11737-9_2) | Link to Computing Maximal Bisimulations

• FDR into The Cloud

  Thomas Gibson−Robinson and A.W. Roscoe

  In Communicating Process Architectures. 2014.

  Details about FDR into The Cloud | BibTeX data for FDR into The Cloud | Download Samples.zip of FDR into The Cloud | Download ClusterFDR.pdf of FDR into The Cloud