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

  • Nestor Cataño Department of Computer Sciences, The University of York, U.K.

Resumen

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.

 

Cómo citar
Cataño, N. (2005). Combining symbolic execution and model checking to reduce dynamic program analysis overhead. Revista Colombiana De Computación, 6(1), 1-15. Recuperado a partir de https://revistas.unab.edu.co/index.php/rcc/article/view/1069

Descargas

La descarga de datos todavía no está disponible.
Publicado
2005-06-01
Sección
Artículo de investigación científica y tecnológica