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>
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:ri-22629 |
| Date | January 2001 |
| Creators | Fredlund, Lars-Åke |
| Publisher | SICS |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Doctoral thesis, monograph, info:eu-repo/semantics/doctoralThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | SICS dissertation series, 1101-1335 ; 29 |
Page generated in 0.0025 seconds