Skip to Main content Skip to Navigation
Reports

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

Néstor Cataño 1
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : By using symbolic execution techniques in the framework of the Java PathFinder model checker, we show that some Java program statements are unable to change the current state of certain offline observer, and so it is useless to instrument them. The observer is given as a finite-state automaton and we considered safety properties.
Document type :
Reports
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00070735
Contributor : Rapport de Recherche Inria <>
Submitted on : Friday, May 19, 2006 - 9:27:50 PM
Last modification on : Saturday, January 27, 2018 - 1:31:29 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:48:40 PM

Identifiers

  • HAL Id : inria-00070735, version 1

Collections

Citation

Néstor Cataño. Combining symbolic execution and model checking to reduce dynamic program analysis overhead. RR-5263, INRIA. 2004, pp.31. ⟨inria-00070735⟩

Share

Metrics

Record views

154

Files downloads

257