University of Leicester

informatics

RESEARCH STUDENT — Tom Gransden MComp Computer Science (University of Leicester)

Ph.D Student
G1Computer Science Building
Department of Informatics,
University of Leicester,
University Road,
Leicester,
LE1 7RH.

T: +44 (0)116 252 3883
F: +44 (0)116 252 3883
E: tg153 (AT) le.ac.uk

About Me

Having begun my undergraduate studies at Leicester in 2008, I graduated in 2012 with an MComp in Computer Science.
I am now working under the supervision of Dr. Neil Walkinshaw and Prof. Rajeev Raman on my PhD: Boosting Automated Reasoning by Mining Existing Proofs.
My PhD studies are funded by a PhD studentship from the College of Science and Engineering PhD Studentship Scheme.

Research Interests

I am researching the topic of tactic mining for Interactive Theorem Provers (ITP's) in an attempt to provide better automation than is currently available. Users conduct proofs in ITP's by entering a finite sequence of proof steps - these can be thought of as functions that either solve a proof or advances the proof state in some way. What I am investigating is how we can apply machine learning techniques to libraries of these proof step sequences. If we can infer useful models from these examples, then hopefully we can use this newly learned information to automate the proofs of new conjectures. This method could be reasonabily applied to any ITP that uses tactics, and has a library of existing proofs that could be mined.

Away from the topics of my PhD, I am mostly interested in the theoretical side of Computer Science. Artificial Intelligence interests me a lot, and I was fortunate enough to be able to learn about computer chess for my 3rd year project. In addition to researching the key concepts, I implemented a chess game in Java, with my own GUI and game engine. If anyone is interested I can try and dig out my old code.

I am also interested in Formal Verification. For my masters dissertation, I used the SPIN model checker to verify some Service Oriented Computing protocols that were specified in a domain specific language. The main tasks were the representation of the models in PROMELA, and the formulation of the desired properties in Linear Temporal Logic.

Publications and Talks

2013

Thomas Gransden
Boosting Automated Reasoning by Mining Existing Proofs [paper][slides][poster]
Automated Reasoning Workshop 2013
Dundee, Scotland

2014

Thomas Gransden, Neil Walkinshaw and Rajeev Raman
Mining State-Based Models from Proof Corpora [preprint - (arXiv)][paper - (SpringerLink)][data][slides][bibtex]
Conferences on Intelligent Computer Mathematics 2014 (Mathematical Knowledge Management Track)
Coimbra, Portugal

2015

Thomas Gransden
Combining SEPIA and ML4PG [paper][slides][poster]
Automated Reasoning Workshop 2015
Birmingham, England

Thomas Gransden, Neil Walkinshaw and Rajeev Raman
SEPIA: Search for Proofs Using Inferred Automata [preprint - (arXiv)][paper - (SpringerLink)][data][slides][bibtex]
Conference on Automated Deduction (CADE-25)
Berlin, Germany

Software

I have written a few software tools over the course of my research. They can be seen at my bitbucket page
The main component of my research is SEPIA, a technique to automatically prove Coq theorems using Extended Finite State Machines..

Teaching Assistance

I have provided teaching assistance for the following modules:

  • CO2012 - Software Project Management and Professionalism
  • CO1001 - Logic and Problem Solving
  • CO3098 - Web Technologies
  • CO7206 - Software Reengineering
  • CO1005 - Data Structures and Development Environments
  • CO1019 - Databases and Web Applications

Author: Tom Gransden (tg153 (AT) le.ac.uk), T: +44 (0)116 252 3883.
University of Leicester 12th November 2012. Last modified: 29th January 2016, 14:16:00.
Informatics Web Maintainer. Any opinions expressed on this page are those of the author.