Context-aware code certification

One challenging issue in automated software engineering is to ensure safety of software execution in changing contexts. In such a scenario, various users, the "code consumers", download an application from a remote server and execute it in their heterogeneous environments. In this paper, a generic meta-level framework (C³) that allows easy adaptation to different contexts for automated safety certification of annotated programs is presented. Context-dependent safety requirements are decoupled from the program specification. The Floyd-Hoarc verification method is extended, and a verification condition generator for deriving generic safety preconditions in terms of generic safety predicates is devised and implemented. The generated safety conditions are simplified and transformed into a negated normal form. This translates the safety verification task into the equivalent task to disprove the existence of a counter example in relation to the selected context. One distinguishing feature of C³ is that safety contexts are meta-level interface specifications. Lifting maps the proof tasks onto the meta-level. Context-dependent safety checking is performed by meta-level reasoning and constraint-solving. A proof of concept implementation was applied to automatically certify absence of context-specific runtime errors and to identify bugs in several cases