Semantics, Modelling and Verification

– University of Geneva –


The development of complex and reliable software systems requires rigorous methods for modelling, designing and verifying them.
The Semantics, Modelling and Verification (SMV) group is a research laboratory involved in the design of formalisms dedicated to the analysis of properties of systems, as well as the automatic generation of their code and of pertinent test cases.
A coherent set of tools has been developed by the group to apply the methods to software-intensive systems.

The SMV lab is part of the Centre Universitaire d’Informatique and the Computer Science Department of the University of Geneva.

Programming languages
Software engineering
Formal methods
Program verification
Model checking


Prof. Didier Buchs, Head of the laboratory

Dr. Dimitri Racordon, Postdoctoral researcher

Damien Morard, Phd student

Aurélien Coet, Phd student

Dr. Steve Hostettler, Senior Lecturer


The SMV lab is in charge of teaching the following courses at the University of Geneva:

Software modelling and verification
Formal methods
Advanced formal methods
Concurrency and repartition
Programming languages semantics

Student Projects

We currently have several propositions for students who would be interested in doing bachelor or master projects with us:

  • Development of a tool to define the semantic rules of programming languages and to derive them mechanically (for an example of a similar approach using the sequent calculus, see this).
  • Design and implementation of a static analysis tool to check that the variables in a program respect the definite assigment property.
  • Design and implementation of an approach for the modelling of substructural type systems with Petri nets. Examples of languages that use such type systems are Rust and Pony.
  • Development of a tool for the visualization of Hero Nets. Hero Nets are a special kind of high-level Petri Nets which can manipulate higher order functions as tokens.
  • Design and implementation of a tool to detect memory leaks in Swift programs. Good C/C++ skills are preferable for this project, as it will require to hack the Swift runtime.
  • Design and implementation of an approach to analyse and report the complexity of type checking on a program’s expressions.

Students are of course also welcome to come and see us with their own ideas for projects.

Past Student Projects

Former Members

Former members of the SMV lab:

Stefan Klikovits
Alban Linard
David Lawrence
Edmundo López Bóbeda
Alexis Marechal
Maximilien Colange
Mihai-Lica Pura
Steve Hostettler
Qin Zhang
Matteo Risoldi
Ang Chen
Levi Lúcio
Andrey Berlizev - Andy sadly left us in April 2009
Luis Pedro
Paula Mangas
David Hurzeler
Adel Besrour
Shane Sendall
Stanislav Chachkov
Jacques Flumet
Julie Vachon
Cécile Péraire
Giovanna Di Marzo
Stéphane Barbey
Pascal Racloz
Jarle Hulaas
Nicolas Guelfi
Sandro Costa
Mathieu Buffo
Olivier Biberstein


Our mail address is:

Semantics, Modelling & Verification Laboratory  
University of Geneva  
Battelle Bat. A  
Route de Drize 7  
CH-1227 Carouge  

You can also contact us by email at: