12.00, Seminar Hall
Parametrised complexity of concurrent shared memory systems
Prakash Saivasan
Univ. of Kaiserlautern, Germany.
04-10-16

---

Abstract

Model checking of concurrent programs communicating via shared memory is an interesting and a hard problem. When recursive processes are involved the problem is undecidable. Even if we consider only finite state systems, the problem is known to be PSPACE-complete. One way to overcome this difficulty is to give up on completeness and look at approximate analysis. One popular approximate analysis is that of bounded context switching. A context switch occurs if a thread gives away control for another thread to be scheduled. In bounded context switch analysis, only those behaviours in which the number of context switches are bounded are considered. This problem is known to be NP-Complete. In this talk we will look at the parametrised complexity analysis of the verification of concurrent programs communicating via shared memory, under the bounded context switch restriction.