Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels
Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés prati...
Main Author: | Clochard, Martin |
---|---|
Other Authors: | Université Paris-Saclay (ComUE) |
Language: | fr |
Published: |
2018
|
Subjects: | |
Online Access: | http://www.theses.fr/2018SACLS071/document |
Similar Items
-
Preuves par raffinement de programmes avec pointeurs
by: Tafat, Asma
Published: (2013) -
Environnement pour le développement et la preuve de correction systèmatiques de programmes parallèles fonctionnels
by: Tesson, Julien
Published: (2011) -
BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms
by: Fortin, Jean
Published: (2013) -
Nouvelles techniques pour l'instanciation et la production des preuves dans SMT
by: Barbosa, Haniel
Published: (2017) -
Aide à la construction et l'évaluation des preuves mathématiques déductives par les systèmes d'argumentation
by: Boudjani, Nadira
Published: (2018)