I am a Research Associate at the University of  Edinburgh, UK.  My research interests are formal methods, theorem proving, network security, proof strategies graphical languages and lemma discovery.

Research

RasE
This project aims to formalise safety and security proprieties of software-defined networking (SDN).  We are, in particular, interested in designing a formal framework which is able to reason about a SDN formalisation with respect to attacks and network resources.

Tacny
State of the art program verifiers are often classified as auto-active: they rely on powerful SMT solvers to discharge proof obligations, and when they fail, the user will guide the proof in the program text through annotations.  The Tacny project aims to develop a language within the Dafny program verifier to allow users to encode reusable proof strategies. Potential advantages include: reuse of verification patterns, meaning improved automation and reduced development time; reduction of annotation overhead, i.e. the code to annotation factor is reduced; and more readable program text as low-level proof guidance can be hidden in the tactics.

Tinker 
We are interested in developing a graphical language for proof strategies (PSGraph language). The Tinker tool, which is the 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. 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
2017
  • Gudmund Grov and Yuhui Lin.  The Tinker tool for graphical tactic development. In Software Tools for Technology Transfer, pages 1-17, DOI: 10.1007/s10009-017-0452-7, 2017 
2016
    • 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.
    2011 - 2015
    • 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