Teaching Deductive Verification in Why3 to Undergraduate Students

Sandrine Blazy

doi:10.1007/978-3-030-32441-4_4

Home
Submit
Browse all HAL
Inria publications
Search
Services
Help
OpenAccess
- Inria supporting open science

Conference papers

Teaching Deductive Verification in Why3 to Undergraduate Students

Sandrine Blazy ^{1, 2, 3}

1 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires

2 UR1 - Université de Rennes 1

3 CELTIQUE - Software certification with semantic analysis

Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL

Sandrine Blazy ^{1, 2, 3} AuthorId : 793190

Author Employer institution : Université de Rennes 1 IdHAL : sandrine-blazy ORCID : https://orcid.org/0000-0002-0189-0223

1 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires (Avenue du général Leclerc Campus de Beaulieu 35042 RENNES CEDEX - France) StructId : 490899

UR1 - Université de Rennes 1 (2 rue du Thabor - CS 46510 - 35065 Rennes cedex - France) StructId : 105160
- UNIV-RENNES - Université de Rennes (France) StructId : 528860
INSA Rennes - Institut National des Sciences Appliquées - Rennes (20, avenue des Buttes de Coësmes - CS 70839 - 35708 Rennes cedex 7 - France) StructId : 117606
- INSA - Institut National des Sciences Appliquées (France) StructId : 301232
- UNIV-RENNES - Université de Rennes (France) StructId : 528860
UBS - Université de Bretagne Sud (BP 92116 - 56321 Lorient cedex - France) StructId : 172265
ENS Rennes - École normale supérieure - Rennes (Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz - France) StructId : 247362
Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France) StructId : 300009
CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France) StructId : 411575
CNRS - Centre National de la Recherche Scientifique : UMR6074 (France) StructId : 441569
IMT Atlantique - IMT Atlantique Bretagne-Pays de la Loire (Campus Brest : Technopôle Brest-Iroise CS 8381829238 BREST Cedex 3 - Campus Nantes : 4, rue Alfred Kastler- La chantrerie 44300 NANTES - Campus Rennes : 2 Rue de la Châtaigneraie, 35510 CESSON SEVIGNE - France) StructId : 481355
- IMT - Institut Mines-Télécom [Paris] (37-39 Rue Dareau, 75014 Paris - France) StructId : 302102

2 UR1 - Université de Rennes 1 (2 rue du Thabor - CS 46510 - 35065 Rennes cedex - France) StructId : 105160

UNIV-RENNES - Université de Rennes (France) StructId : 528860

3 CELTIQUE - Software certification with semantic analysis (Campus de Beaulieu 35042 Rennes cedex - France) StructId : 491212

Inria Rennes – Bretagne Atlantique (Campus de beaulieu 35042 Rennes cedex - France) StructId : 419153
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France) StructId : 300009
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL (France) StructId : 491188
- IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires (Avenue du général Leclerc Campus de Beaulieu 35042 RENNES CEDEX - France) StructId : 490899
  - UR1 - Université de Rennes 1 (2 rue du Thabor - CS 46510 - 35065 Rennes cedex - France) StructId : 105160
    - UNIV-RENNES - Université de Rennes (France) StructId : 528860
  - INSA Rennes - Institut National des Sciences Appliquées - Rennes (20, avenue des Buttes de Coësmes - CS 70839 - 35708 Rennes cedex 7 - France) StructId : 117606
    - INSA - Institut National des Sciences Appliquées (France) StructId : 301232
    - UNIV-RENNES - Université de Rennes (France) StructId : 528860
  - UBS - Université de Bretagne Sud (BP 92116 - 56321 Lorient cedex - France) StructId : 172265
  - ENS Rennes - École normale supérieure - Rennes (Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz - France) StructId : 247362
  - Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France) StructId : 300009
  - CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France) StructId : 411575
  - CNRS - Centre National de la Recherche Scientifique : UMR6074 (France) StructId : 441569
  - IMT Atlantique - IMT Atlantique Bretagne-Pays de la Loire (Campus Brest : Technopôle Brest-Iroise CS 8381829238 BREST Cedex 3 - Campus Nantes : 4, rue Alfred Kastler- La chantrerie 44300 NANTES - Campus Rennes : 2 Rue de la Châtaigneraie, 35510 CESSON SEVIGNE - France) StructId : 481355
    - IMT - Institut Mines-Télécom [Paris] (37-39 Rue Dareau, 75014 Paris - France) StructId : 302102

Document type :

Conference papers

Domain :

Computer Science [cs] / Programming Languages [cs.PL]

Complete list of metadatas

https://hal.inria.fr/hal-02362306
Contributor : Sandrine Blazy <>
Submitted on : Wednesday, November 13, 2019 - 6:23:47 PM
Last modification on : Wednesday, August 5, 2020 - 3:48:25 AM

Identifiers

HAL Id : hal-02362306, version 1
DOI : 10.1007/978-3-030-32441-4_4

Collections

Citation

Sandrine Blazy. Teaching Deductive Verification in Why3 to Undergraduate Students. FM Tea (Formal Methods Teaching), Oct 2019, Porto, Portugal. pp.52-66, ⟨10.1007/978-3-030-32441-4_4⟩. ⟨hal-02362306⟩

Teaching Deductive Verification in Why3 to Undergraduate Students

Identifiers

Collections

Citation

Export

Metrics

61

Contact Legal Notice Personal Data

Teaching Deductive Verification in Why3 to Undergraduate Students

Identifiers

Collections

Citation

Export

Share

Metrics

61

Contact Legal Notice Personal Data