A framework for reasoning about Erlang code

• Main Author: Fredlund, Lars-Åke
• Format: Doctoral Thesis
• Language: English
• Published: SICS 2001
• Subjects: Computer and Information Science; Data- och informationsvetenskap
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:ri:diva-22629

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>