Formalizing Semantics with an Automatic Program Verifier

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01067197
Contributor : Claude Marché <>
Submitted on : Tuesday, September 23, 2014 - 10:55:34 AM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Wednesday, December 24, 2014 - 8:53:05 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01067197, version 1

Collections

Citation

Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Formalizing Semantics with an Automatic Program Verifier. 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria. ⟨hal-01067197⟩

Share

Metrics

Record views

977

Files downloads

508