דן רסין, הרצאה סמינריונית למגיסטר
יום רביעי, 24.5.2017, 11:00
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 existing tools for concurrent verification.