Semantics, Modeling & Verification

Webpage of the Semantics, Modeling & Verification team at University of Geneva

Developing complex and reliable software systems requires rigorous methods for modelling, designing and verifying them. The SMV group is involved in designing dedicated formalisms that are semantically well described in order to make analysis of system properties possible, to automatically produce code and to select pertinent test cases. A coherent set of tools has been developed in order to apply our methods to software-intensive systems.

Bachelor projects

The SMV group is currently creating an automated plant growing system connected to the Internet of Things (IoT). The system consists of single-board computers (Raspberry Pi), various sensors (light, distance, temperature, humidity) and actuators (water pumps). Currently various different software libraries are necessary to interact with these peripheral devices locally, while remote access to the sensor readings is not possible.

The SMV group is currently developing CREST, a graphical modeling language for the design of home automation, automatic plant growing and similar systems. While the first version of the language is being implemented in Python, a graphical editor is necessary for user friendly interaction.

Job Offers

There is currently no job.

Domains of Activity

Domains of Application


Didier Buchs Professor
Stefan Klikovits Ph.D. Student
Alban Linard Post-doc
Dimitri Racordon Ph.D. Student
Steve Hostettler Senior Lecturer

Former Members



Our mail address is:

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


Our team uses the following tools:

A new member of the Semantics, Modeling and Verification team should create accounts in all the services above, and request to become a member of our team in BitBucket and GitHub.