Automatisation des preuves et synthèse des types pour la théorie des ensembles dans le contexte de TLA+
Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués....
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | en |
| Published: |
2014
|
| Subjects: | |
| Online Access: | http://www.theses.fr/2014LORR0208/document |