Controllers for the Verification of Communicating Multi-pushdown Systems
Multi-pushdowns communicating via queues are formal models of multi-threaded programs communicating via channels. They are turing powerful and much of the work on their verification has focussed on under-approximation techniques. Any error detected in the under-approximation implies an error in the system. However the successful verification of the under-approximation is not as useful if the system exhibits unverified behaviours. Our aim is to design controllers that observe/restrict the system so that it stays within the verified under-approximation. We identify some important properties that a good controller should satisfy. We consider an extensive under-approximation class, construct a distributed controller with the desired properties and also establish the decidability of verification problems for this class.
Unable to display preview. Download preview PDF.
- 1.Alur, R., Madhusudan, P.: Adding nesting structure to words. Journal of the ACM 56, 16:1–16:43 (2009)Google Scholar
- 4.Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg, G. (ed.) Handbook of Graph Grammars, pp. 313–400. World Scientific (1997)Google Scholar
- 5.Cyriac, A.: Verification of Communicating Recursive Programs via Split-width. PhD thesis, ENS Cachan (2014), http://www.lsv.ens-cachan.fr/~cyriac/download/Thesis_Aiswarya_Cyriac.pdf
- 7.Cyriac, A., Gastin, P., Narayan Kumar, K.: Controllers for the Verification of Communicating Multi-pushdown Systems. Technical report (2014), http://hal.archives-ouvertes.fr/
- 8.Cyriac, A., Gastin, P., Narayan Kumar, K.: Verifying Communicating Multi-pushdown Systems. Technical report (January 2014), http://hal.archives-ouvertes.fr/hal-00943690
- 13.La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS, pp. 161–170. IEEE Computer Society Press (2007)Google Scholar
- 17.Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 283–294. ACM (2011)Google Scholar