Formalizing Semantics with an Automatic Program Verifier
| Autor: | Martin Clochard, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich |
|---|---|
| Přispěvatelé: | Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Dimitra Giannakopoulou and Daniel Kroening |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: | |
| Zdroj: | 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE) 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2014, Vienna, Austria HAL |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|