Linas Laibinis, Ph.D.

Department of Computer Science
Åbo Akademi University
Lemminkäisenkatu 14A
20520 Turku
FINLAND

Email: llaibini@abo.fi 

Phone: +358 2 2154048 (work), +358 (0)40 7795395 (mobile) 

Fax: +358 2 2154732

Some facts from curriculum vitae:

In 1989 I received my M.Sc. degree in Applied Mathematics from VilniusUniversity, Lithuania. I then spent some years as a researcher in the Mathematics and Cybernetics department of Moscow State University. From 1994 to 2000 I was Ph.D. student at ?bo Akademi University/TUCS in Turku, Finland. I got my PhD degree in April 2000. I am working in the Programming Methods Group at the Computer Science Department. 

Teaching:

This semester I am teaching the Software Safety course. The link to the official course page is here.

Research interests:

• mechanisation of the Refinement Calculus
• interactive environments for proof and/or program construction

Publications:

• Fault Tolerance in a Layered Architecture: A General Specification Pattern in B
  L. Laibinis and E. Troubitsyna,
  
• TUCS technical report No.609 (abstract,pdf file). To appear in Proceedings of Conference on Software Engineering and Formal Methods (SEFM 2004).
  Refinement of Fault Tolerant Control Systems in B
  L. Laibinis and E. Troubitsyna,
  
• TUCS technical report No.603 (abstract,pdf file). To appear in Proceedings of SAFECOMP 2004.
  Specification Variables: Between the Angel and the Demon
  L. Laibinis, J. von Wright,
  
• TUCS technical report No.412 (abstract,Postscript file).
  Mechanised Formal Reasoning About Modular Programs
  L. Laibinis,
  
• TUCS PhD Dissertation No.24, (available as PDF file )
  Functional Procedures in Higher-Order Logic
  L. Laibinis, J. von Wright,
  
• In M. Aagaard, J. Harrison (Eds.), Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, August 2000, Portland, USA. Springer-Verlag, Lecture Notes in Computer Science, number 1869, pg. 372-387, 2000. Earlier version can be found as TUCS technical report No.252 (abstract,Postscript file).
  Mechanising Procedures in HOL
  L. Laibinis,
  
• TUCS technical report No.253 (abstract,Postscript file).
  Developing Components in the Presence of Re-entrance
  L. Mikhajlov, E.Sekerinski and L.Laibinis,
  
• TUCS technical report No.239 (abstract,Postscript file). 
• Proceedings of World Congress on Formal Methods'99 (FM'99), Toulouse, September 1999.
  What's in a Specification?
  L. Laibinis, J. von Wright,
  
• In J.Grundy, M.Schwenke, T.Vickers (Eds.), Proceedings of International Refinement Workshop & Formal Methods Pacific'98, September 1998, Canberra, Australia. Springer-Verlag, pg. 180-192, 1998. Earlier version can be found as TUCS technical report No.174 (abstract,Postscript file).
  Context handling in the Refinement Calculus framework
  L. Laibinis, J. von Wright,
  
• In U. M. Haveraaen, O. Owe (Eds.), Proceedings of the 8th Nordic Workshop on Programming Theory, December 1996, Oslo, Norway. Research Report 248, Department of Informatics, University of Oslo. Extended version can be found as TUCS technical report No.118 (abstract, Postscript file).
  Using Lattice Theory in Higher Order Logic
  L. Laibinis,
  
• In J. von Wright, J. Grundy, J. Harrison (Eds.), Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, August 1996, Turku, Finland. Springer-Verlag, Lecture Notes in Computer Science, number 1125, pg. 315-330, 1996.