Gradual verification of event-driven programs (FWOAL684)

More and more, computer applications need to be concurrent, to deal with multiple input streams and to utilize multi-core hardware, and distributed, to access an ever growing range of consumer and business services in the cloud and in corporate networks. The de- velopment of such programs is encumbered by concurrency pitfalls such as race conditions and deadlocks, and distribution hazards such as connection failures and the lack of a single coordinating entity. A promising foundation for such programs is actor-based concurrency with asynchronous message passing, which rules out low-level data races and deadlocks, and promotes applications that deal gracefully with communication failures. However, it is not a panacea: the event-based model is particularly vulnerable to higher-level safety and liveness issues, such as unanticipated message interleavings and distributed delegation loops.

In this project, we propose to investigate these challenges and develop reasoning principles and tooling strategies to address them. Such tooling will include static verifica- tion tools to efficiently establish mathematical certainty of critical application correctness properties. However, to allow for quick independent evolution, we will design our tooling strategy from the ground up to enable gradual verification, where static verification is integrated seamlessly with run-time enforcement approaches. This novel combined approach promises to significantly improve the ease of delivering correct event-based systems.

Keywords:Databases, Evolution of language, Programming languages, Mobile Computing, Artificial Intelligence, Serious games, Web systems, Software agents

Disciplines:Programming languages not elsewhere classified, Applied mathematics in specific fields