From processes to automata: compactification theorem
1 : Laboratoire Méthodes Formelles
(LMF)
* : Auteur correspondant
Institut National de Recherche en Informatique et en Automatique, CentraleSupélec, Université Paris-Saclay, Centre National de la Recherche Scientifique, Ecole Normale Supérieure Paris-Saclay
4, avenue des Sciences, 91190, Gif-sur-Yvette -
France
When working on concurrency, synchronization can be very hard to deal with. This paper aims to outline the construction of a compactification theorem which simplifies a lot some proofs about the synchronization of a finite (but unbounded) number of normalizable processes in the framework HOL-CSP.
| Type : | : | typdoc_34556 |
| Langue du texte intégral | : | anglais |
| Date de production, écriture | : | 31/10/2025 |
| Thématiques | : | Posters et DEMO |
| Mots-Clés | : | formal verification ; isabelle ; HOL ; CSP ; proof |
| PDF version | : |  PDF version |
- Poster
