Wed 22 Jan 2020 11:13 - 11:35 at Ile de France III (IDF III) - Complexity / Decision Procedures Chair(s): Roopsha Samanta
We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is Pspace-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change
10:30 - 11:35 | Complexity / Decision ProceduresResearch Papers at Ile de France III (IDF III) Chair(s): Roopsha Samanta Purdue University | ||
10:30 21mTalk | The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space Research Papers Yannick Forster Saarland University, Fabian Kunze Saarland University, Marc Roth Saarland University and MMCI and Merton College, Oxford University Link to publication DOI Pre-print Media Attached | ||
10:51 21mTalk | Complexity and Information in Invariant Inference Research Papers Yotam M. Y. Feldman Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university Link to publication DOI Media Attached | ||
11:13 21mTalk | Parameterized Verification under TSO is PSPACE-Complete Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Rojin Rezvan Sharif University Link to publication DOI |