Improved verification techniques for concurrent systems

Toman V. 2021. Improved verification techniques for concurrent systems. IST Austria.

Download
OA toman_th_final.pdf 2.92 MB

Thesis | PhD | Published | English
Series Title
IST Austria Thesis
Abstract
The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness.
Publishing Year
Date Published
2021-10-31
Page
166
ISSN
IST-REx-ID

Cite this

Toman V. Improved verification techniques for concurrent systems. 2021. doi:10.15479/at:ista:10199
Toman, V. (2021). Improved verification techniques for concurrent systems. IST Austria. https://doi.org/10.15479/at:ista:10199
Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” IST Austria, 2021. https://doi.org/10.15479/at:ista:10199.
V. Toman, “Improved verification techniques for concurrent systems,” IST Austria, 2021.
Toman V. 2021. Improved verification techniques for concurrent systems. IST Austria.
Toman, Viktor. Improved Verification Techniques for Concurrent Systems. IST Austria, 2021, doi:10.15479/at:ista:10199.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2021-11-08
MD5 Checksum
4f412a1ee60952221b499a4b1268df35

Source File
File Name
Access Level
Restricted Closed Access
Date Uploaded
2021-11-08
MD5 Checksum
9584943f99127be2dd2963f6784c37d4

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar