Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/139089
Title: A SESSION LOGIC FOR RELAXED COMMUNICATION PROTOCOLS
Authors: MIRELA ANDREEA COSTEA
Keywords: session logic, programming languages, communication protocols, software verification, concurrency, separation logic
Issue Date: 23-Aug-2017
Citation: MIRELA ANDREEA COSTEA (2017-08-23). A SESSION LOGIC FOR RELAXED COMMUNICATION PROTOCOLS. ScholarBank@NUS Repository.
Abstract: This thesis tackles the formalization of concurrent programs, where the synchronization among processes is mainly achieved via message passing. Since message passing is a preferred avenue for achieving high performance in distributed applications, ensuring its safe and correct design and implementation is crucial, yet challenging. The challenge mostly comes from the complex interaction schemes normally used in a distributed system. Furthermore, to achieve better concurrency, most of today’s systems have the benefit of supporting and employing a variety of synchronization primitives besides message passing, increasing thus the complexity of communicating programs. Previous approaches, largely based on session types, provide a concise way to express protocol specifications and a lightweight approach for checking their implementation. However, the previous solutions mostly rely on implicit synchronization for achieving safe concurrency, and are based on the less precise types rather than logical formulae. This thesis proposes a session logic which offers an expressive, yet simple specification language to describe the communication between multiple participants in the presence of explicit synchronization. It also proposes proposes the necessary means to incorporate this logic into a verification framework, to check for protocol conformance and communication safety (type safety, race and deadlock freedom).
URI: http://scholarbank.nus.edu.sg/handle/10635/139089
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
CosMA.pdf1.22 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

96
checked on Oct 18, 2018

Download(s)

57
checked on Oct 18, 2018

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.