Publikation: Heuristic-Guided Counterexample Search in FLAVERS
Lade...
Dateien
Datum
2004
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering - SIGSOFT '04/FSE-12. New York, New York, USA: ACM Press, 2004, pp. 201-210. ISBN 1-58113-855-5. Available under: doi: 10.1145/1029894.1029922
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Heuristic search, counterexamples, FLAVERS
Konferenz
The 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering - SIGSOFT '04/FSE-12, 31. Okt. 2004 - 6. Nov. 2004, Newport Beach, CA, USA
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
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 on Foundations of software engineering - SIGSOFT '04/FSE-12. 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. New York, New York, USA: ACM Press, 2004, pp. 201-210. ISBN 1-58113-855-5. Available under: doi: 10.1145/1029894.1029922BibTex
@inproceedings{Tan2004Heuri-5597,
year={2004},
doi={10.1145/1029894.1029922},
title={Heuristic-Guided Counterexample Search in FLAVERS},
isbn={1-58113-855-5},
publisher={ACM Press},
address={New York, New York, USA},
booktitle={Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering - SIGSOFT '04/FSE-12},
pages={201--210},
author={Tan, Jianbin and Avrunin, George S. and Clarke, Lori A. and Zilberstein, Shlomo and Leue, Stefan}
}RDF
<rdf:RDF
xmlns:dcterms="http://purl.org/dc/terms/"
xmlns:dc="http://purl.org/dc/elements/1.1/"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:bibo="http://purl.org/ontology/bibo/"
xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
xmlns:foaf="http://xmlns.com/foaf/0.1/"
xmlns:void="http://rdfs.org/ns/void#"
xmlns:xsd="http://www.w3.org/2001/XMLSchema#" >
<rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/5597">
<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:rights>Attribution-NonCommercial-NoDerivs 2.0 Generic</dc:rights>
<dc:contributor>Leue, Stefan</dc:contributor>
<dc:creator>Clarke, Lori A.</dc:creator>
<dc:creator>Leue, Stefan</dc:creator>
<dc:contributor>Tan, Jianbin</dc:contributor>
<dc:language>eng</dc:language>
<dcterms:issued>2004</dcterms:issued>
<dc:format>application/pdf</dc:format>
<dc:creator>Avrunin, George S.</dc:creator>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<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>
<dc:contributor>Clarke, Lori A.</dc:contributor>
<dc:contributor>Zilberstein, Shlomo</dc:contributor>
<dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc-nd/2.0/"/>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5597"/>
<dc:contributor>Avrunin, George S.</dc:contributor>
<dc:creator>Zilberstein, Shlomo</dc:creator>
<dcterms:title>Heuristic-Guided Counterexample Search in FLAVERS</dcterms:title>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:41Z</dcterms:available>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:41Z</dc:date>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5597/1/Heuristic_Guided_Counterexample_Search_in_FLAVERS.pdf"/>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5597/1/Heuristic_Guided_Counterexample_Search_in_FLAVERS.pdf"/>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
