Controllers for the Verification of Communicating Multi-Pushdown Systems

Cyriac Aiswarya 1, * Paul Gastin 2, 3 K. Narayan Kumar 4
* Corresponding author
3 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : 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 con- troller 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download
Contributor : C. Aiswarya <>
Submitted on : Friday, August 22, 2014 - 11:50:02 PM
Last modification on : Thursday, January 11, 2018 - 6:23:37 AM
Long-term archiving on : Thursday, November 27, 2014 - 1:55:54 PM


Files produced by the author(s)


  • HAL Id : hal-01057525, version 1



Cyriac Aiswarya, Paul Gastin, K. Narayan Kumar. Controllers for the Verification of Communicating Multi-Pushdown Systems. 25th International Conference on Concurrency Theory (CONCUR'14),, 2014, Rome, Italy. pp.297-311. ⟨hal-01057525⟩



Record views


Files downloads