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 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
Contact Details Email: y.lin (AT) hw (dot) ac (dot) uk |