Relational properties for specification and verification of C programs in Frama-C
Les techniques de vérification déductive fournissent des méthodes puissantes pour la vérification formelle des propriétés exprimées dans la Logique de Hoare. Dans cette formalisation, également connue sous le nom de sémantique axiomatique, un programme est considéré comme un transformateur de prédic...
| Main Author: | |
|---|---|
| Other Authors: | |
| Language: | en |
| Published: |
2019
|
| Subjects: | |
| Online Access: | http://www.theses.fr/2019SACLC065/document |