Automated Modular Verification for Race-Free Channels with Implicit and Explicit Synchronization

Andreea Costea, Wei-Ngan Chin, Florin Craciun, Shengchao Qin

Ensuring the correctness of software for communication centric programs is important but challenging. Previous approaches, based on session types, have been intensively investigated over the past decade. They provide a concise way to express protocol specifications and a lightweight approach for checking their implementation. Current solutions are based on only implicit synchronization, and are based on the less precise types rather than logical formulae. In this paper, we propose a more expressive session logic to capture multiparty protocols. By using two kinds of ordering constraints, namely "happens-before"

picture_as_pdf flag

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment