Verification of asynchronous concurrency and the shaped stack constraint

Thesis

In this dissertation, we study the verification of concurrent programs written in the programming language Erlang using infinite-state model-checking. Erlang is a widely used, higher order, dynamically typed, call-by-value functional language with algebraic data types and pattern-matching. It is further augmented with support for actor concurrency, i.e. asynchronous message passing and dynamic process creation.

With decidable model-checking in mind, we identify actor co...

Expand abstract

Authors: Kochems, J

• Publication date: 2014
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: Oxford University, UK
• Language: English
• Keywords: Infinite-State Model-Checking; Well-Structured Transition Systems; Verification; Petri Nets; Infinite-State Systems Verification; Asynchronous Message Passing; Erlang; Concurrent Pushdown Systems
• Subjects: Applications and algorithms; Computing; Computer science (mathematics); Theory and automated verification