Department of Information Technology

Controllers for the verification of communicating multi-pushdown systems


Aiswarya Cyriac, Uppsala University, Sweden

Date and Time

Tuesday, June 11th, 2014 at 14:45.


Polacksbacken, room 4306


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. One way to utilise the verification of an under-approximation is to restrict the system using a controller to stay within the under-approximation. We identify some important properties that a good controller should satisfy. We consider an extensive under-approximation class and construct a distributed controller with the desired properties for this class.

Updated  2014-06-09 15:52:34 by Mohamed Faouzi Atig.