Improving representative computation in ExpliSAT

Hana Chockler, Dmitry Pidan, Sitvanit Ruah

Research output: Chapter in Book/Report/Conference proceedingConference paper

2 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationHardware and Software: Verification and Testing
Subtitle of host publication9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings
EditorsValeria Bertacco, Axel Legay
PublisherSpringer International Publishing
Number of pages6
ISBN (Print)9783319030760
Publication statusPublished - 1 Dec 2013
Event9th Haifa Verification Conference, HVC 2013 - Haifa, United Kingdom
Duration: 5 Nov 20137 Nov 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8244 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference9th Haifa Verification Conference, HVC 2013
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Improving representative computation in ExpliSAT'. Together they form a unique fingerprint.

Cite this