FM /

Formal Methods - FM Research Group

Department of Computer Science and Engineering, Chalmers and the University of Gothenburg

go to Administrative area (private)

About this page:

This is the page of the Formal Methods group at Chalmers University of Technology/University of Gothenburg. The page has not been updated recently, except for the list of group members. An overhaul is on its way, please check back in a few weeks for up-to-date content. In the meanwhile, feel free to refer to the members' personal pages for information about the group's recent activities.



Before summer, 2013 we got the following papers accepted:

  • A framework for conflict analysis of normative texts written in controlled natural language. In Journal of Logic and Algebraic Programming, 82(5-7):216-240, 2013, authored by Krasimir Angelov, John C. Camilleri, and Gerardo Schneider.
  • Reachability analysis of complex planar hybrid systems. In Science of Computer Programming journal, 78(12):2511-2536, 2013, authored by Hallstein Hansen, Gerardo Schneider, and Martin Steffen.
  • Migration of an on-premise application to the cloud: Experience report, presented at ESOCC'13 (Malaga, Spain), published in LNCS, vol 8135, pp. 227-241. Authors: Pavel Rabetski and Gerardo Schneider (based on Pavel's master thesis).
  • Automatic testing of real-time graphics systems, presented at TACAS'13 (Rome, Italy), published in LNCS vol 7795, pp. 465-479. Authors: Robert Nagy, Gerardo Schneider, and Aram Timofeitchik (based on Robert and Aram's master thesis).
  • A Unified Approach for Static and Runtime Verification: Framework and Applications, presented at ISoLA 2012, published in LNCS 7609. Authors: Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider.

Check our calendar!


  • The award-winning Vampire theorem prover;
  • The loop invariant generation package Aligator;
  • The formal verification platform KeY;


Upcoming Events:

Project Proposals for Bachelor and Master Students

We offer student projects on various topics of formal verification, with particular emphasis on:

  • formal software verification: model checking, runtime verification, deductive software verificaton and verification-based testing;
  • automated reasoning: decision procedures, first-order theorem proving, inductive theorem proving and theory exploration;
  • contract verification: specification and analysis of contract.

If you are interested in working us, just drop by our offices or send us an email (see email address below).

FM Courses:

To be soon completed.