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|
|Deposited By:||INVALID USER|
|Deposited On:||17 Jun 2008|
|Last Modified:||04 Dec 2013 15:11|
Repository Staff Only: item control page