Welcome to Reiner Hähnle's Home Page

I am a professor in the Division of Software Engineering and Technology within the Department of Computer Science and Engineering of Chalmers University of Technology.

I lead the research group in Software Engineering using Formal Methods.

You find me in Room 5449 in the EDIT Building on Chalmers Main Campus in Rännvägen 6B. My office phone number is +46-31-772-1061. My email address is (replace "*" with "@") reiner*chalmers.se.

• HATS: Highly Adaptable & Trustworthy Software Using Formal Models
  An Integrated Project in FP7-ICT-2007-3 Theme "Forever Yours"
  
  
• The KeY project is concerned with Integrating Object Oriented Design and Formal Verification.
  In collaboration with Bernhard Beckert at University of Koblenz and Peter Schmitt at University of Karlsruhe

  The book on KeY is now available - the definite source for all information related to the KeY project

  Verification of Object-Oriented Software: The KeY Approach Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (Eds.) 15 chapters and 2 appendices, xxix + 658 pages ISBN: 3-540-68977-X Springer-Verlag, LNCS 4334 - BibTeX - Book Website - Online edition (Springer LINK)

  
  
  

• CHARTER: Critical and High Assurance Requirements Transformed through Engineering Rigour, a collaborative project funded by the ARTEMIS Embedded Computing Systems Initiative
  
  
  
• COST Action IC0701: Formal Verification of Object-Oriented Software.
  
  
• COST Action IC0901: Rich Model Toolkit - An Infrastructure for Reliable Computer Systems
  
  

Publications , see also DBLP and Google Scholar

Research Interests:

• Current: generally, Formal Methods in Software Engineering - specifically:
  • Formal verification of object-oriented software, see KeY and COST Action IC0701
  • Formal modeling and specification of highly adaptive software systems, see HATS
  • Automated Test Case Generation by Symbolic Execution, see KeY-Test
  • Debugging and Program Understanding by Visualization of Symbolic Eexecution, see Symbolic Execution Debugger
• Past:
  • Automated Theorem Proving, mainly TABLEAUX methods
  • Formal Reasoning in Many-Valued Logic

• PC-member of 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Dakar, Senegal, April 2010
  
  
• PC co-chair of International Joint Conference on Automated Reasoning (IJCAR), held as part of Federated Logic Conferences (FLoC), Edinburgh, UK, July 2010
  
  
• PC-member 6th International Verification Workshop (VERIFY), Edinburgh, UK July 2010
  
  
• PC-member of Fourth International Conference on Tests and Proofs TAP'10, Malaga, Spain, July 2010
  
  
• PC member of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), held as part of European Joint Conferences on Theory and Practice of Software (ETAPS), Saarland, Germany, March 26 - April 4 2011
  
  

• I am on the editorial board of the Journal of Automated Reasoning published by Springer-Verlag. The journal solicits contributions on all aspects of mechanized reasoning including all kinds of applications such as verification. Feel free to contact me if you are interested to submit an article.
  
  
• I am on the editorial board of FoLLI Publications on Logic, Language, and Information, a subseries of Springer LNAI
  

  If you would like to suggest a conference proceedings or a monography as part of this series, please contact me



• I am in the editorial board of the journal Multiple-Valued Logic and Soft Computing, OCP Science
  
  
• Trustee and Vice-President of Conference on Automated Deducation (CADE), Inc.
  
  
• Ex-officio member (on behalf of IJCAR 2010) of the Steering Committee of the TABLEAUX conference series, Conference Co-founder, Past President of Tableaux 2000-2003
  
  

Teaching (current/future)

• Testing, Debugging, and Verification: 2nd term, Winter 2009, TDA566/DIT082
  
  

Teaching (earlier courses)

• Testing, Debugging, and Verification: 2nd term, Winter 2008, TDA566/DIT082
  
  
• Software Engineering using Formal Methods: 1st term, Winter 2008, TDA292/DIT270
  
  
• Program Verification; 2nd term, Winter 2007, TDA565
  
  
• Software Engineering using Formal Methods; 3rd term, Spring 2003/04/05/06/07 INN170/TIN291
  
  
• Artificial Intelligence; 4th term, Spring 2000/01/02/03/04/05/06/07, INN410/TIN170
  
  
• Graduate Course on Automated Theorem Proving; Winter 2004/05
  
  
• Programmering för Naturvetare, del 2 (Introduction to Programming in Java), INN010, 2001
  
  
• Project Course IT 2; 4th term, Spring 2003, TDA410
  
  

More info on me: Send e-mail to reiner "at" chalmers.se and ask for my CV.

Current PhD students:

Ran Ji works in the HATS project.

Gabriele Paganelli (co-supervisor) works in the CHARTER project.

Angela Wallenburg (Licenciate 2004).

Former PhD students:

Niklas Sörensson (2008) is now an independant consultant for applications of his world-leading SAT solver MiniSat.

Daniel Larsson (Licenciate 2006) works now at QRtech AB.

Tobias Gedell (Licenciate 2006), (PhD 2008, co-supervisor) works now for an international bank.

Wojciech Mostowski (2005) is a postdoctoral fellow at University of Nijmegen.

Thomas Baar (2002) was a senior researcher at Swiss Federal Institute of Technology in Lausanne (EPFL) until 2007 and now works for Tech@Spree.

Martin Giese (2002) is a postdoctoral fellow at University of Oslo, Norway.

Wolfgang Ahrendt (2001) is a Lecturer and my colleague here at Chalmers.