Raisonnement automatisé pour la logique de séparation avec des définitions inductives
La contribution principale de cette thèse est un système de preuve correct et complet pour les implications entre les prédicats inductifs, fréquemment rencontrées lors de la vérification des programmes qui utilisent des structures de données récursives allouées dynamiquement. Nous introduisons un sy...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | en |
| Published: |
2018
|
| Subjects: | |
| Online Access: | http://www.theses.fr/2018GREAM030/document |