Algorithmic Game Semantics and Component−Based Verification
Samson Abramsky · 2003
We present a research programme dedicated to the application of Game Semantics to program analysis and verification. We highlight several recent theoretical results and describe a prototypical software modeling and verification tool. The distinctive novel features of the tool are its ability to handle open programs and the fact that the models it produces are observationally fully abstract. These features are essential in the modeling and verification of software components such as modules. Incidentally, these features also lead to very compact models of programs.