Formal Methods - FM Research Group

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

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.

News:

In July 2014, the paper Hipster: Integrating Theory Exploration in a Proof Assistant, authored by Moa Johansson, Dan Rosen, Nicholas Smallbone and Koen Claessen, received a best paper award at the Conference on Intelligent Computer Mathematics in Coimbra, Portugal.
In October 2013 we got the paper Specification and Verification of Normative texts using C-O Diagrams accepted at the IEEE Transactions on Software Engineering journal, authored by Gregorio Díaz, María Emilia Cambronero, Enrique Martínez, and Gerardo Schneider.
October 15-18, 2013: We have an accepted paper on symbolic execution at the 11th International Symposium on Automated Technology for Verification and Analysis - ATVA 2013, authored by Armin Biere, Jens Knoop, Laura Kovacs and Jakob Zwirchmayr.
September 2013: Three new PhD students have joined the FM group:, Jesus Mauricio Chimento, Evgeny Kotelnikov, and John J. Camilleri.
July 13-19, 2013: We have an invited paper on first-order theorem proving at the 25th International Conference on Computer Aided Verification - CAV 2013, authored by Laura Kovacs and Andrei Voronkov;
July 9, 2013: We have an accepted paper on symbolic execution at the 13th International Workshop on Worst-Case Execution Time Analysis - WCET 2013, authored by Armin Biere, Jens Knoop, Laura Kovacs and Jakob Zwirchmayr;
June 9-14, 2013: We have an accepted paper on inductive theorem proving at the 24th International Conference on Automated Deduction - CADE 2013, authored by Koen Claessen, Moa Johansson, Dan Rosen and Nicholas Smallbone;
May 23, 2013: Two new PhD students, Jesus Mauricio Chimento and Evgeny Kotelnikov, will join the FM group in Fall 2013;

Papers:

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!

Software:

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

Members:

Upcoming Events:

September 30 - October 2, 2013: 12th KeY Symposium 2013
July 5-6, 2013: 5th International Symposium on Symbolic Computation in Software Science - SCSS 2013
July 5-6, 2013: 5th International Symposium on Symbolic Computation in Software Science - SCSS 2013
July 13-14, 2013: 1st Workshop on Interpolation - iPrA 2013
September 24-26, 2013: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - SYNASC 2013
December 14-19, 2013: 19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - LPAR 2013
January 19-21, 2014: 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
September 29 - October 1, 2014: 13th KeY Symposium 2014
October 29-31, 2014: 26th Nordic Workshop on Programming Theory, NWPT '14

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.

Organization:

FM weekly meetings, Wednesdays, at 3pm;
FM mailing list: fm.cse at chalmers.se;
Official Chalmers home page of the FM group: the page is slightly outdated.