---
_id: '10199'
abstract:
- lang: eng
  text: 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.
acknowledged_ssus:
- _id: SSU
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Viktor
  full_name: Toman, Viktor
  id: 3AF3DA7C-F248-11E8-B48F-1D18A9856A87
  last_name: Toman
  orcid: 0000-0001-9036-063X
citation:
  ama: Toman V. Improved verification techniques for concurrent systems. 2021. doi:<a
    href="https://doi.org/10.15479/at:ista:10199">10.15479/at:ista:10199</a>
  apa: Toman, V. (2021). <i>Improved verification techniques for concurrent systems</i>.
    Institute of Science and Technology Austria. <a href="https://doi.org/10.15479/at:ista:10199">https://doi.org/10.15479/at:ista:10199</a>
  chicago: Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.”
    Institute of Science and Technology Austria, 2021. <a href="https://doi.org/10.15479/at:ista:10199">https://doi.org/10.15479/at:ista:10199</a>.
  ieee: V. Toman, “Improved verification techniques for concurrent systems,” Institute
    of Science and Technology Austria, 2021.
  ista: Toman V. 2021. Improved verification techniques for concurrent systems. Institute
    of Science and Technology Austria.
  mla: Toman, Viktor. <i>Improved Verification Techniques for Concurrent Systems</i>.
    Institute of Science and Technology Austria, 2021, doi:<a href="https://doi.org/10.15479/at:ista:10199">10.15479/at:ista:10199</a>.
  short: V. Toman, Improved Verification Techniques for Concurrent Systems, Institute
    of Science and Technology Austria, 2021.
date_created: 2021-10-29T20:09:01Z
date_published: 2021-10-31T00:00:00Z
date_updated: 2025-07-14T09:10:16Z
day: '31'
ddc:
- '000'
degree_awarded: PhD
department:
- _id: GradSch
- _id: KrCh
doi: 10.15479/at:ista:10199
ec_funded: 1
file:
- access_level: open_access
  checksum: 4f412a1ee60952221b499a4b1268df35
  content_type: application/pdf
  creator: vtoman
  date_created: 2021-11-08T14:12:22Z
  date_updated: 2021-11-08T14:12:22Z
  file_id: '10225'
  file_name: toman_th_final.pdf
  file_size: 2915234
  relation: main_file
- access_level: closed
  checksum: 9584943f99127be2dd2963f6784c37d4
  content_type: application/zip
  creator: vtoman
  date_created: 2021-11-08T14:12:46Z
  date_updated: 2021-11-09T09:00:50Z
  file_id: '10226'
  file_name: toman_thesis.zip
  file_size: 8616056
  relation: source_file
file_date_updated: 2021-11-09T09:00:50Z
has_accepted_license: '1'
keyword:
- concurrency
- verification
- model checking
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '166'
project:
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '665385'
  name: International IST Doctoral Program
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '10190'
    relation: part_of_dissertation
    status: public
  - id: '9987'
    relation: part_of_dissertation
    status: public
  - id: '141'
    relation: part_of_dissertation
    status: public
  - id: '10191'
    relation: part_of_dissertation
    status: public
status: public
supervisor:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
title: Improved verification techniques for concurrent systems
type: dissertation
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
year: '2021'
...