A framework for reasoning about Erlang code

Fredlund, Lars-Åke (2001) A framework for reasoning about Erlang code. Doctoral thesis, KTH.



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

Item Type:Thesis (Doctoral)
Additional Information:Trita-IT. AVH ; 01:04, URI: urn:nbn:se:kth:diva-3210
ID Code:3113
Deposited On:17 Jun 2008
Last Modified:04 Dec 2013 15:11

Repository Staff Only: item control page