Controllers for the verification of communicating multi-pushdown systems

Speaker

Aiswarya Cyriac, Uppsala University, Sweden

Date and Time

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

Location

Polacksbacken, room 4306

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. 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.