Technical Report MSC-2018-03

TR#:MSC-2018-03
Class:MSC
Title: Modular Verification of Concurrent Programs via Sequential Model Checking
Authors: Dan Rasin
Supervisors: Orna Grumberg, Sharon Shoham
PDFCurrently accessibly only within the Technion network
Abstract: Verification of concurrent programs is known to be extremely difficult. On top of the challenges inherent in verifying sequential programs, it adds the need to consider a high (typically unbounded) number of thread interleavings. In this work, we utilize the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We introduce a technique which reduces the verification of a concurrent program to a series of verification tasks of sequential programs, without explicitly encoding all the possible interleavings. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional information about the environment in which it operates. Information regarding the environment is gathered during the run of the algorithm, by need.

A unique aspect of our approach is that it exploits a hierarchical structure of the program in which one of the threads, considered ``main'', is being verified as a sequential program. Its verification process initiates queries to its ``environment'' (which may contain multiple threads). Those queries are answered by sequential verification, if the environment consists of a single thread, or, otherwise, by applying the same hierarchical algorithm on the environment.

Our technique is fully automatic, and allows us to use any off-the-shelf sequential model-checker. We implemented our technique in a tool called CoMuS and evaluated it against established tools for concurrent verification. Our experiments show that it works particularly well on hierarchically structured programs.

CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2018/MSC/MSC-2018-03), rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the MSC technical reports of 2018
To the main CS technical reports page

Computer science department, Technion
admin