Home > Research > Publications & Outputs > Quick verification of concurrent programs by it...


Text available via DOI:

View graph of relations

Quick verification of concurrent programs by iteratively relaxed scheduling

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

  • P. Metzler
  • H. Saissi
  • P. Bokor
  • Neeraj Suri
  • Nguyen T.N. (Editor)
  • Rosu G. (Editor)
  • Di Penta M. (Editor)


The most prominent advantage of software verification over testing is a rigorous check of every possible software behavior. However, large state spaces of concurrent systems, due to non-deterministic scheduling, result in a slow automated verification process. Therefore, verification introduces a large delay between completion and deployment of concurrent software. This paper introduces a novel iterative approach to verification of concurrent programs that drastically reduces this delay. By restricting the execution of concurrent programs to a small set of admissible schedules, verification complexity and time is drastically reduced. Iteratively adding admissible schedules after their verification eventually restores non-deterministic scheduling. Thereby, our framework allows to find a sweet spot between a low verification delay and sufficient execution time performance. Our evaluation of a prototype implementation on well-known benchmark programs shows that after verifying only few schedules of the program, execution time overhead is competitive to existing deterministic multi-threading frameworks. © 2017 IEEE.