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 - Formally Verified Programs, Certified Tools and Numerical Computations
2 LRI - Laboratoire de Recherche en Informatique

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.

Domaines: Logique en informatique [cs.LO]

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⟩