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.
Si vous avez des idées de projets, n’hésitez pas à nous en faire part. Nous serons ravi d’en discuter et d’adapter au mieux le sujet pour travailler sur une thématique qui vous intéresse.
Pour tout contact pour l’un de ces projets (ou pour proposer votre projet): damien.morard@unige.ch
Projets de Bachelor
- Création de cartes à l’aide de l’impression 3D pour représenter un langage de programmation.
- Création d’un interprète pour un jeu a but de découverte informatique/algorithmique. L’objectif serait de vérifier que les algorithmes réalisés lors d’une partie de notre jeu soient correctes.
- Création d’une application pour piloter un drone et créer un parcours de vol.
Projets Master
- Hero nets (Higher-order Petri nets): Création d’un outil de visualisation. Les Hero nets ressemblent à des High-level Petri nets à la différence que les tokens peuvent être des higher-order functions.
- Création d’une librairie pour écrire différents types de DD (Decision diagrams).
- Comprendre quels sont les mécanismes des nouveaux langages de programmations qui sont difficiles à appréhender pour les utilisateurs.
Job Offers
There is currently no job.
Domains of Activity
- Model checking
- Programming Language
- Software prototyping
- Model engineering (MDA,UML, model transformation)
Domains of Application
- Concurrent system
- Embedded systems
- Ubiquitous systems
- Safety engineering : System and Human Risk Analysis (in collaboration with the Institute of Occupational Health Sciences, Lausanne)
Members
| Didier Buchs |  |
Professor |      |
| Stefan Klikovits |  |
Post-doc | |
| Dimitri Racordon |  |
Post-doc | |
| Damien Morard |  |
Ph.D. Student | |
| Aurélien Coet |  |
Ph.D. Student | |
| Steve Hostettler |  |
Senior Lecturer | |
Former Members
- 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
Courses
- Modélisation et Vérification
- Outils Formels de Modélisation
- Outils Formels Avancés/Concurrence et répartition
- Sémantique des Langages Informatiques
Contact
Our mail address is:
Semantics, Modeling & Verification Maboratory
University of Geneva
Battelle Bat. A
Route de Drize 7
CH-1227 Carouge
Switzerland
Information
Our team uses the following tools:
- BitBucket for private data, such as paper sources, talk sources, or course sources
- GitHub for our homepage, courses and software
- ResearchGate for our projects and articles
- Overleaf to write papers, that should be put after completion in BitBucket
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.