Mikino: Induction for Dummies (demonstration) - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

Mikino: Induction for Dummies (demonstration)

Adrien Champion
  • Fonction : Auteur
Steven de Oliveira
  • Fonction : Auteur
Keryan Didier
  • Fonction : Auteur

Résumé

Mikino is a simple induction engine over transition systems. It is written in Rust, with a strong focus on ergonomics and user-friendliness. It is accompanied by a detailed tutorial which introduces basic notions such as logical operators and Smt solvers. Mikino and its companion tutorial target developers with little to no experience with verification in general and induction in particular. This work is an attempt to educate developers on what a proof by induction is, why it is relevant for program verification, why it can fail to (dis)prove a candidate invariant, and what to do in this case.
Fichier principal
Vignette du fichier
jfla22_paper_23.pdf (567.41 Ko) Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte

Dates et versions

hal-03626850 , version 1 (31-03-2022)

Identifiants

  • HAL Id : hal-03626850 , version 1

Citer

Adrien Champion, Steven de Oliveira, Keryan Didier. Mikino: Induction for Dummies (demonstration). 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.254-260. ⟨hal-03626850⟩

Collections

JFLA2022
69 Consultations
132 Téléchargements

Partager

Gmail Facebook X LinkedIn More