Comment implémenter le support des goroutines dans go2pins

From LRDE

Revision as of 17:23, 9 November 2020 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.