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.