Wiki Agenda Contact English version

A Formally Verified Interpreter for the Shell-like Language CoLiS

The shell-like language CoLiS is described with abstract syntax trees and a formal semantics defined by inductive predicates. An interpreter is written in Why3 and proved correct and complete with respect to the semantics.

Auteurs: Nicolas Jeannerod

Catégories: Inductive predicates / Ghost code

Outils: Why3

Références: CoLiS project

see also the index (by topic, by tool, by reference, by year)

download ZIP archive
why3doc index

why3doc index

Generated by why3doc 0.87+git