A Pragmatic Type System for Deductive Verification

Jean-Christophe Filliâtre 1, 2 Léon Gondelman 1, 2 Andrei Paskevich 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : In the context of deductive verication, it is customary today to handle programs with pointers using either separation logic, dynamic frames, or explicit memory models. Yet we can observe that in numerous programs, a large amount of code ts within the scope of Hoare logic, provided we can statically control aliasing. When this is the case, the code correctness can be reduced to simpler verication conditions which do not require any explicit memory model. This makes verication conditions more amenable both to automated theorem proving and to manual inspection and debugging. In this paper, we devise a method of such static aliasing control for a programming language featuring nested data structures with mutable components. Our solution is based on a type system with singleton regions and eects, which we prove to be sound.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01256434
Contributeur : Jean-Christophe Filliâtre <>
Soumis le : lundi 1 février 2016 - 10:24:14
Dernière modification le : mardi 17 avril 2018 - 09:08:49
Document(s) archivé(s) le : vendredi 11 novembre 2016 - 21:08:23

Fichier

main (1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01256434, version 3

Citation

Jean-Christophe Filliâtre, Léon Gondelman, Andrei Paskevich. A Pragmatic Type System for Deductive Verification. 2016. 〈hal-01256434v3〉

Partager

Métriques

Consultations de la notice

458

Téléchargements de fichiers

143