Wiki Agenda Contact Version française

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.

Authors: Nicolas Jeannerod

Topics: Inductive predicates / Ghost code

Tools: Why3

References: 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