Weakest Safe Context Synthesis by Symbolic Game Semantics and Logical Abduction
Aleksandar S. Dimovski · 2025
Game semantics provides fully abstract (sound and complete) models for open program fragments with undefined, non-local, identifiers (e.g. library functions). This is achieved by using the "most general" models for undefined identifiers, i.e. the most generic context in which the program fragment will be inserted. Given a safety property as an assertion, we want to find the most permissive models of undefined identifiers, i.e. the weakest safe context, that are sufficient to ensure safety of the given program fragment.