A Unified Approach to Compositional Software Modelling, Analysis and Verification

Software modelling, analysis and verificationcomprises many sophisticated but often disparate techniques such asmodel checking, static analysis or testing. Although takenindividually such techniques are effective in targeting particularproblems, a combined approach is always recommended. However, in theabsence of a unified framework, integration can be awkward and mayfail to achieve true synergy. Using Game Semantics as a commontheoretical foundation we can provide such a unified framework forsoftware modelling, analysis and verification. The modularity ofextant techniques is often limited, which restrains theirscalability. Game Semantics is intrinsically compositional and recentresearch has already shown how it can be used to model subprograms inmodular fashion, especially the subtle interplay between proceduresand state that cannot be represented using extant techniques. However,compositional modelling is only the first step towards compositionalverification. We plan to further develop means for compositionalreasoning, that is methods of specifying properties of executionenvironments and of verifying that subprograms plug together withoutviolating their mutual assumptions. This can be achieved using eitherprogram logics or type systems. Building on existing research, we aimto push compositional methods beyond correctness verification, intomore intensional analyses such as estimating time of execution, memoryrequirements or resource usage. We also aim to expand beyond staticverification, by examining compositional approaches totesting. Throughout the programme, foundational and applied researchwill naturally intertwine and play off each other.