I am a Research Associate  in Computer Science within the School of Mathematical and Computer Sciences at Heriot-Watt University in Edinburgh, UK. I work in the Dependable Systems Group. My research interests are Formal Methods, Theorem Proving, ProofStrategies, Graphical Languages, Lemma Discovery. Currently I am working on Tinker: A Graph Based Proof Strategy Tool.

Research

Tinker 
We are interested in developing  a graphical language for proof strategies (PSGraph language). The Tinker tool, which is a first implementation of PSGraphs. It adopts a generic theorem prover independent framework. We have currently connected it to both Isabelle and ProofPower. I was a member of the Tinker development team, providing an implementation of the PSGraph language. Here, I developed the underlying core and GUI, and integrated the language with new theorem provers. 

POPPA (Proof Obligation Proofs Patched Automatically)
This is my phD research topic. This work is part of the EPSRC funded AI4FM project. It aimed to improve the proof automation for formal methods using a high-level proof-planning theorem proving techniques, i.e. rippling. I targeted at one family of proofs from one popular formal methods, called Even-B invariant proofs. I was, in particular, interested in the case when proofs, and then we developed proof patches based on the high-level guidance for rippling to discover missing lemmas, apply a case split or unfold definitions.

Experiences

Supervision for Undergraduate Summer Projects                               June 2015 - Aug 2015
School of Mathematical & Computer Sciences, Heriot-Watt University 

CISA Seminar Organiser                                                  Feb 2013 - May 2014
School of Informatics, the University of Edinburgh          

Demonstrator                                                                                              Sep 2012 - Apr 2013
School of Informatics, the University of Edinburgh
Courses: Object-Oriented Programming, Computer Programming Skills and Concepts, Automated Reasoning.

Translator
- TheoryMine Edinburgh, UK May 2011 - Nov 2011
  Translated the brochure and the TheoryMine website to a Chinese version.
- Majinate  ltd York, UK May 2010 - Aug 2010
  Translated and reviewed the exam questions for the Accredited Symbian Developer program.

Events

Program Committee & Local Arrangements and Publicity Chair: 

Education


PhD in Informatics [pdf]                                                                                  Oct 2010 - Nov 2014
School of Informatics, the University of Edinburgh                                   Edinburgh, UK

MSc in Software Engineering with Distinction [pdf]                                Oct 2009 - Sep 2010
Department of Computer Science, University of York  York, UK

BSc in Software Engineering                                                                          Sep 2003 - Jun 2007
Department of Software Engineering, Fujian Normal University  FuJian, China

Publication
  • Yuhui Lin, Gudmund Grov and Rob Arthan. Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC. In Journal of Formalized Reasoning, Volume 9, No 2 (2016), pages 69-130. 
  • Gudmund Grov, Yuhui Lin and Pierre Le Bras.The Tinker GUI for graphical proof strategies (tool demo). To appear in 3rd Workshop on Formal Integrated Development Environment, 2016.
  • Gudmund Grov, Yuhui Lin, Leon McGregoer, Vytautas Tumas and Duncan Cameron. Extending the Dafny IDE with tactics and dead annotation analysis (tool demo). To appear in 3rd Workshop on Formal Integrated Development Environment, 2016.
  • Gudmund Grov, Yuhui Lin and Vytautas Tumas. Mechanised Verification Patterns for Dafny. In the 21st International Conference on Formal Methods (FM 2016). To appear.
  • Yuhui Lin, Gudmund Grov, Colin O'Halloran and Priiya G.  A super industrial application of PSGraph. In the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), volume 9675 of LNCS, pages 319–325, Springer, 2016.
  • Yibo Liang, Yuhui Lin and Gudmund Grov. ‘The Tinker’ for Rodin. In the 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), volume 9675 of LNCS, pages 262–268, Springer, 2016. 
  • Yuhui Lin, Pierre Le Bras and Gudmund Grov. Developing & Debugging Proof Strategies by Tinkering. In the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 of LNCS, pages 573–579, Springer, 2016.
  • Pierre Le Bras, Yuhui Lin and Gudmund Grov. Tinker: A Graph Based Proof Strategy System.  In AI4FM 2015 (extended abstract) 
  • G. Grov, A. Kissinger and Y. Lin. Tinker, Tailor, Solver, Proof. In Proceedings of Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 2014. Electronic Proceedings of Theoretical Computer Science 167, pp. 23-34. 
  • G. Grov, A. Kissinger and Y. Lin. A Graphical Language for Proof Strategies. In Logic for Programming Artificial Intelligence and Reasoning, LPAR-19th, Stellenbosch, South Africa, 2013.
  • Y. Lin, A. Bundy, and G. Grov. The Use of Rippling to Automate Event-B Invariant Preservation Proofs. In Alwyn Goodloe and Suzette Person, editors, NASA Formal Methods—4th International Symposium, NFM 2012, volume 7226 of LNCS, pages 231–236. Springer, 2012.
  • Y. Lin, A. Bundy, and G. Grov. The Use of Rippling to Automate Event-B Invariant Preservation Proofs. In IJCAR Workshop on Automated Theory eXploration (ATX 2012), Manchester, UK, June 2012.
  • A. Bundy, G. Grov and Y. Lin. Productive Use of Failure in Top-down Formal Methods. In Proceedings of 18th Automated Reasoning Workshop, University of Glasgow, Department of Computer Science, Technical Report TR-2011-327, A. Miller & R. Kirwan (Eds), 2011, pp. 13-14.

Contact Details

Email: y.lin (AT) hw (dot) ac (dot) uk
Phone: +44 (0)131 451 4183
AddressRoom G.59 Earl Mountbatten Building School of Mathematical & Computer Sciences; 
Computer Science Heriot-Watt University 
Edinburgh EH14 4AS 
United Kingdom