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
References: CoLiS project
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
Generated by why3doc 0.87+git