Difference between revisions of "Publications/martin.19.seminar/fr"
From LRDE
Line 4: | Line 4: | ||
| year = 2019 |
| year = 2019 |
||
| number = 1910 |
| number = 1910 |
||
− | | resume = go2pins est un outil utilisé pour interfacer un programme Go avec des outils de vérification formelle. À l'aide d'une série de transformations, un programme Go est compilé vers un programme au comportement identique, mais exposant une interface permettant d'itérer dans l'espace d'états de celui ci. |
+ | | resume = go2pins est un outil utilisé pour interfacer un programme Go avec des outils de vérification formelle. À l'aide d'une série de transformations, un programme Go est compilé vers un programme au comportement identique, mais exposant une interface permettant d'itérer dans l'espace d'états de celui ci. Cependantgo2pins ne gère actuellement pas les programmes utilisant des goroutines, qui permettent l'exécution parallèle de fonctions. Dans ce rapport, nous présentons les solutions envisagées pour implémenter ce comportement dans go2pins, ainsi que les problèmes rencontrés. |
| type = techreport |
| type = techreport |
||
| id = martin.19.seminar |
| id = martin.19.seminar |
Latest revision as of 17:23, 9 November 2020
- Auteurs
- Antoine Martin
- Type
- techreport
- Année
- 2019
- Numéro
- 1910
Résumé
go2pins est un outil utilisé pour interfacer un programme Go avec des outils de vérification formelle. À l'aide d'une série de transformations, un programme Go est compilé vers un programme au comportement identique, mais exposant une interface permettant d'itérer dans l'espace d'états de celui ci. Cependantgo2pins ne gère actuellement pas les programmes utilisant des goroutines, qui permettent l'exécution parallèle de fonctions. Dans ce rapport, nous présentons les solutions envisagées pour implémenter ce comportement dans go2pins, ainsi que les problèmes rencontrés.