Combining symbolic execution and model checking to reduce dynamic program analysis overhead

Abstract

This paper addresses the problem of reducing the runtime monitoring overhead for programs where ¯ne-grained monitoring of events is required. To this end we complement model checking techniques with symbolic reasoning methods and show that, under certain circumstances, code fragments do not a®ect the validity of underlying properties. We consider safety properties given as regular expressions on events generated by the program. Further, we show how our framework can be extended to consider programs with cycles. We sample our presentation with the aid of the Java PathFinder model checker [13].

Keywords: model checking, Java PathFinder, symbolic reasoning, instrumentation, monitoring, invariant strengthening.