Write a Blog >>

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 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

10:30 - 11:35: Research Papers - Complexity / Decision Procedures at Ile de France III (IDF III)
Chair(s): Roopsha SamantaPurdue University
POPL-2020-Research-Papers10:30 - 10:51
Yannick ForsterSaarland University, Fabian KunzeSaarland University, Marc RothSaarland University and MMCI and Merton College, Oxford University
Link to publication DOI Pre-print Media Attached
POPL-2020-Research-Papers10:51 - 11:13
Yotam FeldmanTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university
Link to publication DOI Media Attached
POPL-2020-Research-Papers11:13 - 11:35
Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Rojin RezvanSharif University
Link to publication DOI