On Bounded Reachability Analysis of Shared Memory Systems

Authors Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan

Thumbnail PDF


  • Filesize: 0.49 MB
  • 13 pages

Document Identifiers

Author Details

Mohamed Faouzi Atig
Ahmed Bouajjani
K. Narayan Kumar
Prakash Saivasan

Cite AsGet BibTex

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On Bounded Reachability Analysis of Shared Memory Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 611-623, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


This paper addresses the reachability problem for pushdown systems communicating via shared memory. It is already known that this problem is undecidable. It turns out that undecidability holds even if the shared memory consists of a single boolean variable. We propose a restriction on the behaviours of such systems, called stage bound, towards decidability. A k stage bounded run can be split into a k stages, such that in each stage there is at most one process writing to the shared memory while any number of processes may read from it. We consider several versions of stage-bounded systems and establish decidability and complexity results.
  • Reachability problem
  • Pushdown systems
  • Counter systems


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Mohamed Faouzi Atig. Model-checking of ordered multi-pushdown automata. Logical Methods in Computer Science, 8(3), 2012. Google Scholar
  2. Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR, volume 5201 of Lecture Notes in Computer Science, pages 356-371. Springer, 2008. Google Scholar
  3. Mohamed Faouzi Atig and Tayssir Touili. Verifying parallel programs with dynamic communication structures. In CIAA, volume 5642 of Lecture Notes in Computer Science, pages 145-154. Springer, 2009. Google Scholar
  4. Pierre Chambart and Ph. Schnoebelen. Post embedding problem is not primitive recursive, with applications to channel systems. In FSTTCS, volume 4855 of Lecture Notes in Computer Science, pages 265-276. Springer, 2007. Google Scholar
  5. Bruno Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178-186, 1991. Google Scholar
  6. Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 124-140. Springer, 2013. Google Scholar
  7. Matthew Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  8. Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, volume 7358 of Lecture Notes in Computer Science, pages 260-276. Springer, 2012. Google Scholar
  9. J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley series in computer science. Addison-Wesley, 1979. Google Scholar
  10. Rodney R. Howell and Louis E. Rosier. An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. J. Comput. Syst. Sci., 34(1):55-74, 1987. Google Scholar
  11. Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. Google Scholar
  12. Salvatore La Torre, Parthasarathy Madhusudan, and Gennaro Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE Computer Society, 2007. Google Scholar
  13. Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of Lecture Notes in Computer Science, pages 93-107. Springer, 2005. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail