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

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	709-727
Number of pages	19
Journal	International Journal on Software Tools for Technology Transfer
Volume	17
Issue number	6
DOIs	https://doi.org/10.1007/s10009-014-0314-5
Publication status	Published - 1 Nov 2015
Externally published	Yes

Keywords

Automated theorem proving
Case study
Deductive verification
Formal specification

Access to Document

10.1007/s10009-014-0314-5

Cite this

@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

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

Abstract

Keywords

Access to Document

Fingerprint

Cite this