Combining symbolic execution and model checking to reduce dynamic program analysis overhead
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 th...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Universidad Autónoma de Bucaramanga
2005-06-01
|
| Series: | Revista Colombiana de Computación |
| Online Access: | https://revistas.unab.edu.co/index.php/rcc/article/view/1069 |
| id |
doaj-bebeacb132e24e3aaaf74ed586223b5d |
|---|---|
| record_format |
Article |
| spelling |
doaj-bebeacb132e24e3aaaf74ed586223b5d2020-11-25T03:24:55ZengUniversidad Autónoma de BucaramangaRevista Colombiana de Computación1657-28312539-21152005-06-0161Combining symbolic execution and model checking to reduce dynamic program analysis overheadNestor Cataño0Department of Computer Sciences, The University of York, U.K.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. https://revistas.unab.edu.co/index.php/rcc/article/view/1069 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Nestor Cataño |
| spellingShingle |
Nestor Cataño Combining symbolic execution and model checking to reduce dynamic program analysis overhead Revista Colombiana de Computación |
| author_facet |
Nestor Cataño |
| author_sort |
Nestor Cataño |
| title |
Combining symbolic execution and model checking to reduce dynamic program analysis overhead |
| title_short |
Combining symbolic execution and model checking to reduce dynamic program analysis overhead |
| title_full |
Combining symbolic execution and model checking to reduce dynamic program analysis overhead |
| title_fullStr |
Combining symbolic execution and model checking to reduce dynamic program analysis overhead |
| title_full_unstemmed |
Combining symbolic execution and model checking to reduce dynamic program analysis overhead |
| title_sort |
combining symbolic execution and model checking to reduce dynamic program analysis overhead |
| publisher |
Universidad Autónoma de Bucaramanga |
| series |
Revista Colombiana de Computación |
| issn |
1657-2831 2539-2115 |
| publishDate |
2005-06-01 |
| description |
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.
|
| url |
https://revistas.unab.edu.co/index.php/rcc/article/view/1069 |
| work_keys_str_mv |
AT nestorcatano combiningsymbolicexecutionandmodelcheckingtoreducedynamicprogramanalysisoverhead |
| _version_ |
1724599032474501120 |