Return to search

A framework for reasoning about Erlang code

We present a framework for formal reasoning about the behaviour of software written in Erlang, a functional programming language with prominent support for process based concurrency, message passing communication and distribution. The framework contains the following key ingredients: a specification language based on the mu-calculus and first-order predicate logic, a hierarchical small-step structural operational semantics of Erlang, a judgement format allowing parameterised behavioural assertions, and a Gentzen style proof system for proving validity of such assertions. The proof system supports property decomposition through a cut rule and handles program recursion through well-founded induction. An implementation is available in the form of a proof assistant tool for checking the correctness of proof steps. The tool offers support for automatic proof discovery through higher--level rules tailored to Erlang. As illustrated in several case / <p>Trita-IT. AVH ; 01:04, URI: urn:nbn:se:kth:diva-3210</p>
Date January 2001
CreatorsFredlund, Lars-Åke
Source SetsDiVA Archive at Upsalla University
Detected LanguageEnglish
TypeDoctoral thesis, monograph, info:eu-repo/semantics/doctoralThesis, text
RelationSICS dissertation series, 1101-1335 ; 29

Page generated in 0.0173 seconds