Années:
2009
(
IRL Ensimag)
Co-encadrant:
David Monniaux
Sujet: Model-checking de programmes Java
Résumé: 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
-