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 computer 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. Steve Hostettler, Senior Lecturer

Damien Morard, Phd student

Aurélien Coet, Phd student

Dr. Dimitri Racordon, Research associate


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:

  • Visualisation of High-Level Petri Nets.
  • Implementation of a lazy functional programming language.
  • Development of a game to teach the basic principles of logic.
  • Development of a forward model checker for CTL formulae.
  • Application of model checking to verify the correctness of security protocols.
  • Development of a tool for the visualisation of error traces in Rust programs.

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:

Emmanouela Stachtiari 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: or