Romain Salles

Model-checking de programmes Java

Saturday 1 January 2011

Years: 2009 (IRL Ensimag)
Co-supervisor: David Monniaux
Subject: Model-checking de programmes Java
Abstract:

Ce sujet était au départ inspiré du sujet de Loïc Crétin l’année précédente. Vu les difficultés que posaient l’intégration des briques de base, nous avons décidé de nous passer d’un certain nombre d’entre elles : pas de front-end de compilateur complexe, pas de bibliothèque externe. Cette-fois, nous travaillons avec le byte-code Java, et la seule bibliothèque est ASM, qui permet de lire simplement ce byte-code. L’idée est de générer du code pour le model-checker NuSMV, et de l’utiliser pour prouver des propriétés sur des programmes booléens.

La traduction a été entièrement implémentée, et testée sur des exemples tirés d’un cours de programmation concurrente : différentes variantes de l’algorithme de Dekker (une correcte, et d’autres avec problèmes de synchronisation comme famine, dead-lock, propriété d’exclusion mutuelle violée, ...). L’outil a prouvé la version correcte et trouvé les contre-exemples pour les autres.

2024

Preprints, Working Papers, ...

ref_biblio: S Aiello, A Albert, M Alshamsi, S. Alves Garre, Z Aly, et al.. Astronomy potential of KM3NeT/ARCA. 2024. ⟨hal-04480224⟩
Accès au bibtex

2023

Preprints, Working Papers, ...

ref_biblio: Angel Abusleme, Thomas Adam, Shakeel Ahmad, Rizwan Ahmed, Sebastiano Aiello, et al.. The Design and Technology Development of the JUNO Central Detector. 2023. ⟨hal-04338602⟩
Accès au bibtex

2022

Journal articles

ref_biblio: Angel Abusleme, Thomas Adam, Shakeel Ahmad, Rizwan Ahmed, Sebastiano Aiello, et al.. Mass testing and characterization of 20-inch PMTs for JUNO. Eur.Phys.J.C, 2022, 82 (12), pp.1168. ⟨10.1140/epjc/s10052-022-11002-8⟩. ⟨hal-03737679⟩
Accès au bibtex

2017

Journal articles

ref_biblio: Mabrouka El Hachani, < Mabrouka, El Hachani. Bibliothèque et liens intergénérationnels : Situations d’interactions avec tablettes,. Interfaces numériques, 2017, 6, ⟨10.3199/RIN.1.1-n⟩. ⟨hal-01700491⟩
Accès au bibtex

2016

Journal articles

ref_biblio: Bingrui Xu, Jalel Chergui, Seungwon Shin ·, Damir Juric. Three-dimensional simulations of viscous folding in diverging microchannels. Microfluidics and Nanofluidics, 2016, 20 (10), ⟨10.1007/s10404-016-1803-5⟩. ⟨hal-02610529⟩
Accès au texte intégral et bibtex

2014

Conference papers

ref_biblio: Mirsad Buljubasic, Michel Vasquez, Haris Gavranovi ́. Two-phase heuristic for SNCF rolling stock problem. IFORS 2014 : 20th Conference of the International Federation of Operational Research Societies,, Jul 2014, Barcelona, Spain. ⟨hal-01951610⟩
Accès au bibtex

View online : Résumé sur Ensiwiki