Vérification formelle de programmes de génération de données structurées

Le problème général de la preuve de propriétés de programmes impératifs est indécidable. Pour deslangages de programmation et de propriétés plus restrictifs, des sous-problèmes décidables sontconnus. En pratique, grâce à des heuristiques, les outils de preuve de programmes automatisent despreuves qu...

Full description

Bibliographic Details
Main Author: Genestier, Richard
Other Authors: Besançon
Language:fr
Published: 2016
Subjects:
Coq
003
Online Access:http://www.theses.fr/2016BESA2041/document