Change search
ReferencesLink to record
Permanent link

Direct link
A framework for reasoning about Erlang code
Number of Authors: 1
2001 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

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

Place, publisher, year, edition, pages
2001, 4. , 233 p.
, SICS Dissertation Series
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-14817OAI: diva2:1036111
Trita-IT. AVH ; 01:04, URI: urn:nbn:se:kth:diva-3210Available from: 2016-10-13 Created: 2016-10-13

Open Access in DiVA

fulltext(1224 kB)0 downloads
File information
File name FULLTEXT01.pdfFile size 1224 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

ReferencesLink to record
Permanent link

Direct link