On Optimally Combining Static and Dynamic Analyses For Intensional Program Properties

The goal of algorithmic program verification is to automatically prove programs correct with respect to logical specifications. Program verification techniques can be broadly classified as either static or dynamic. Informally, static techniques try to establish the proof of correctness without executing the program. Program errors, if any, are detected prior to execution. However, there is no guarantee that a proof of correctness will be found, even when such a proof may actually exist. Dynamic techniques, on the other hand, insert run-time checks in the program that trigger an exception if the specification is violated during program execution.1 Though these checks cause run-time overheads, they remove the burden of proving a program correct prior to execution. Given the complementary nature of static and dynamic approaches to program verification, it is natural to consider a combined approach that first checks the program statically, and in case the correctness cannot be established, introduces run-time checks in the program wherever necessary. A number of such combined or hybrid approaches such as gradual typing [1,2], hybrid type checking [3], soft contract verification [4] have been proposed in the literature. Though these approaches differ in their details, the common thread is that they use static checking wherever possible, and only defer to run-time checks where necessary. These run-time checks are expressed using dynamic contracts [5, 6]. Though dynamic contracts suffice for enforcing functional correctness properties, many program properties, such as data-race freedom, deadlock freedom, and information-flow security, need additional mechanisms for run-time enforcement. In particular, these properties require defining an instrumented language semantics that tracks extra information about how computations execute, beyond that which would appear in a standard semantics for the language. The extra information tracked is property-specific; for instance, data-race freedom requires keeping track of a may-happen-before ordering relation for reads and writes in the program. In general, such program properties that refer to “how computations execute" are dubbed as intensional properties. Dynamic analyses for checking intensional properties can have large overheads since, in addition to checking dynamic contracts, the analysis is also required to maintain and update additional program state. A hybrid approach can help reduce the run-time overheads, but the design of such hybrid approaches is more involved in the instrumented semantics setting. It does not suffice to reduce the number of dynamic contracts in the program. We also need to reduce the additional information tracked by the semantics. Fortunately, static analysis can help us ensure that only the necessary information is tracked in addition to ensuring that dynamic contracts are introduced only