I am a Research Associate in the Systems Research Group at the University of  St Andrews.  My research interests are cloud computing, automated reasoning and network security.


Adaptive Brokerage for the Cloud (ABC)

Robustness as Evolvability (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.

Tactic for Dafny (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 / Proof Strategy Graph (PSGraph)
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. 

Proof Obligation Proofs Patched Automatically (POPPA)
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.


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.

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


Program Committee & Local Arrangements and Publicity Chair: 


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

  • W. Chen, Y. Lin, V. Galpin, V. Nigam, M. Lee, and D. AspinallFormal Analysis of Sneak-Peek: A Data Centre Attack and its Mitigations. In IFIP SEC’18. 33rd IFIP TC-11 SEC 2018.
  • G. Grov and Y. 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 
    • Y. Lin, G. Grov and R. 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. 
    • G. Grov, Y. Lin and P. Le Bras. The Tinker GUI for graphical proof strategies. In 3rd Workshop on Formal Integrated Development Environment, 2016.
    • G. Grov, Y. Lin, L. McGregoer, V. Tumas and D. Cameron. Extending the Dafny IDE with tactics and dead annotation analysis. In 3rd Workshop on Formal Integrated Development Environment, 2016.
    • G. Grov, Y. Lin and V. Tumas. Mechanised Verification Patterns for Dafny. In the 21st International Conference on Formal Methods (FM 2016). 
    • Y. Lin, G. Grov, C. O'Halloran and P. 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.
    • Y. Liang, Y. Lin and G. 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. 
    • Y. Lin, P. Le Bras and G. 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
    • P. Le Bras, Y. Lin and G. 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.

    Contact Details

    Email: yl205@st-andrews.ac.uk
    JC1.37 - Jack Cole Building, North Haugh, St Andrews KY16 9SX