Modular Reasoning about Concurrent Higher-Order Imperative Programs
Over the last five years, mainstream programming languages such as Java, C#, and Scala have evolved to permit a powerful combination of language features (a) mutable shared data structures, (b) higher-order functions, and (c) concurrency.
These features are all very important for programming in practice. However, the combination of them makes it difficult to write correct and secure programs, and it is therefore very important to develop mathematically-based techniques for formal reasoning about correctness and security of programs with these features.
The ModuRes project will break new ground by developing mathematical models and logic for modular reasoning about programs written in realistic programming languages with all the challenging features (a, b, c). The project will lay the foundation for future software tools, which will be used to improve software practice.
Microsoft Research Cambridge, UK, co-sponsors research (PhD) on Relational Reasoning for Programs using Higher-Order Store.
