Heuristic-Guided Counterexample Search in FLAVERS

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:31096bce1a25e545eacad775d075e9d8

TAN, Jianbin, George S. AVRUNIN, Lori A. CLARKE, Shlomo ZILBERSTEIN, Stefan LEUE, 2004. Heuristic-Guided Counterexample Search in FLAVERS. the 12th ACM SIGSOFT twelfth international symposium. Newport Beach, CA, USA, 31. Okt 2004 - 6. Nov 2004. In: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering - SIGSOFT '04/FSE-12. the 12th ACM SIGSOFT twelfth international symposium. Newport Beach, CA, USA, 31. Okt 2004 - 6. Nov 2004. New York, New York, USA:ACM Press, pp. 201. ISBN 1-58113-855-5

@inproceedings{Tan2004Heuri-5597, title={Heuristic-Guided Counterexample Search in FLAVERS}, year={2004}, doi={10.1145/1029894.1029922}, isbn={1-58113-855-5}, address={New York, New York, USA}, publisher={ACM Press}, booktitle={Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering - SIGSOFT '04/FSE-12}, author={Tan, Jianbin and Avrunin, George S. and Clarke, Lori A. and Zilberstein, Shlomo and Leue, Stefan} }

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/5597"> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5597"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:41Z</dcterms:available> <dc:contributor>Leue, Stefan</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:41Z</dc:date> <dcterms:abstract xml:lang="eng">One of the benefits of finite-state verification (FSV) tools, such as model checkers, is that a counterexample is provided when the property cannot be verified. Not all counterexamples, however, are equally useful to the analysts trying to understand and localize the fault. Often counterexamples are so long that they are hard to understand. Thus, it is important for FSV tools to find short counterexamples and to do so quickly. Commonly used search strategies, such as breadth-first and depth-first search, do not usually perform well in both of these dimensions. In this paper, we investigate heuristic-guided search strategies for the FSV tool FLAVERS and propose a novel two-stage counterexample search strategy. We describe an experiment showing that this two-stage strategy, when combined with appropriate heuristics, is extremely effective at quickly finding short counterexamples for a large set of verification problems.</dcterms:abstract> <dc:creator>Avrunin, George S.</dc:creator> <dcterms:issued>2004</dcterms:issued> <dc:format>application/pdf</dc:format> <dcterms:rights rdf:resource="https://creativecommons.org/licenses/by-nc-nd/2.0/legalcode"/> <dc:creator>Clarke, Lori A.</dc:creator> <dc:rights>deposit-license</dc:rights> <dc:language>eng</dc:language> <dc:contributor>Avrunin, George S.</dc:contributor> <dc:contributor>Tan, Jianbin</dc:contributor> <dcterms:title>Heuristic-Guided Counterexample Search in FLAVERS</dcterms:title> <dc:contributor>Clarke, Lori A.</dc:contributor> <dc:contributor>Zilberstein, Shlomo</dc:contributor> <dc:creator>Leue, Stefan</dc:creator> <dc:creator>Zilberstein, Shlomo</dc:creator> <dcterms:bibliographicCitation>First publ. in: ACM International Symposium on the Foundations of Software Engineering (SIGSOFT), 2004, pp. 201-210</dcterms:bibliographicCitation> <dc:creator>Tan, Jianbin</dc:creator> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Heuristic_Guided_Counterexample_Search_in_FLAVERS.pdf 110

Das Dokument erscheint in:

deposit-license Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: deposit-license

KOPS Suche


Stöbern

Mein Benutzerkonto