Let’s verify this with Why3

François Bobot; Jean Christophe Filliâtre; Claude Marché; Andrei Paskevich

doi:10.1007/s10009-014-0314-5

Let’s verify this with Why3

François Bobot
, Jean Christophe Filliâtre
, Claude Marché
, Andrei Paskevich

CEA/UVSQ/CNRS
INRIA Saclay, Laboratoire de Recherche en Informatique (LRI), Université Paris Sud
INRIA
Université Paris-Saclay

Résultats de recherche: Contribution à un journal › Article › Revue par des pairs

Résumé

We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.

langue originale	Anglais
Pages (de - à)	709-727
Nombre de pages	19
journal	International Journal on Software Tools for Technology Transfer
Volume	17
Numéro de publication	6
Les DOIs	https://doi.org/10.1007/s10009-014-0314-5
état	Publié - 1 nov. 2015
Modification externe	Oui

Accès au document

10.1007/s10009-014-0314-5

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

@article{7fb48f9c6b814aa0930a9dc4d9d81737,

title = "Let{\textquoteright}s verify this with Why3",

abstract = "We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.",

keywords = "Automated theorem proving, Case study, Deductive verification, Formal specification",

author = "Fran{\c c}ois Bobot and Filli{\^a}tre, \{Jean Christophe\} and Claude March{\'e} and Andrei Paskevich",

note = "Publisher Copyright: {\textcopyright} 2014, Springer-Verlag Berlin Heidelberg.",

year = "2015",

month = nov,

day = "1",

doi = "10.1007/s10009-014-0314-5",

language = "English",

volume = "17",

pages = "709--727",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

number = "6",

}

TY - JOUR

T1 - Let’s verify this with Why3

AU - Bobot, François

AU - Filliâtre, Jean Christophe

AU - Marché, Claude

AU - Paskevich, Andrei

PY - 2015/11/1

Y1 - 2015/11/1

N2 - We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.

AB - We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.

KW - Automated theorem proving

KW - Case study

KW - Deductive verification

KW - Formal specification

UR - https://www.scopus.com/pages/publications/84943454863

U2 - 10.1007/s10009-014-0314-5

DO - 10.1007/s10009-014-0314-5

M3 - Article

AN - SCOPUS:84943454863

SN - 1433-2779

VL - 17

SP - 709

EP - 727

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 6

ER -

Let’s verify this with Why3

Résumé

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation