@inbook{04dae324e6aa4b0d906953b5628a256c,
title = "Improving representative computation in ExpliSAT",
abstract = "This paper proposes a new algorithm for computing path representatives in the concolic software verification tool ExpliSAT. A path representative is a useful technique for reducing the number of calls to a decision procedure by maintaining an explicit instantiation of symbolic variables that matches the current control flow path. In the current implementation in ExpliSAT, the whole representative is guessed at the beginning of an execution and then recomputed if it does not match the currently traversed control flow path. In this paper we suggest a new algorithm for computation of a representative, where the instantiation is done {"}on demand{"}, that is, only when a specific value is required in order to determine feasibility. Experimental results show that using representatives improves performance.",
author = "Hana Chockler and Dmitry Pidan and Sitvanit Ruah",
year = "2013",
month = dec,
day = "1",
doi = "10.1007/978-3-319-03077-7_24",
language = "English",
isbn = "9783319030760",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer International Publishing",
pages = "359--364",
editor = "Bertacco, {Valeria } and Axel Legay",
booktitle = "Hardware and Software: Verification and Testing",
note = "9th Haifa Verification Conference, HVC 2013 ; Conference date: 05-11-2013 Through 07-11-2013",
}