Formalizing Semantics with an Automatic Program Verifier

Martin Clochard 1, 2 Jean-Christophe Filliâtre 1, 2 Claude Marché 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 : A common belief is that formalizing semantics of programming languages requires the use of a proof assistant providing (1) a specification language with advanced features such as higher-order logic, inductive definitions, type polymorphism, and (2) a corresponding proof environment where higher-order and inductive reasoning can be performed, typically with user interaction. In this paper we show that such a formalization is nowadays possible inside a mostly-automatic program verification environment. We substantiate this claim by formalizing several semantics for a simple language, and proving their equivalence, inside the Why3 environment.
Type de document :
Communication dans un congrès
Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/hal-01067197
Contributeur : Claude Marché <>
Soumis le : mardi 23 septembre 2014 - 10:55:34
Dernière modification le : jeudi 9 février 2017 - 15:57:01
Document(s) archivé(s) le : mercredi 24 décembre 2014 - 20:53:05

Fichier

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

Identifiants

  • HAL Id : hal-01067197, version 1

Citation

Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier. Dimitra Giannakopoulou and Daniel Kroening. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. Springer, 8471, 2014, Lecture Notes in Computer Science. <hal-01067197>

Partager

Métriques

Consultations de
la notice

513

Téléchargements du document

247