Publikation:

Ultimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution)

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2017

Autor:innen

Greitschus, Marius
Dietsch, Daniel
Heizmann, Matthias
Nutz, Alexander
Schätzle, Claus
Schüssele, Frank
Podelski, Andreas

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
DOI (zitierfähiger Link)
https://doi.org/10.1007/978-3-662-54580-5_31
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

LEGAY, Axel, ed., Tiziana MARGARIA, ed.. Tools and algorithms for the construction and analysis of systems : 23rd international conference, TACAS 2017, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part 2. Berlin: Springer, 2017, pp. 399-403. Lecture Notes in Computer Science. 10206. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-54579-9. Available under: doi: 10.1007/978-3-662-54580-5_31

Zusammenfassung

Ultimate Taipan is a software model checker for C programs. It is based on a CEGAR variant, trace abstraction [7], where program abstractions, counterexample selection and abstraction refinement are based on automata. Ultimate Taipan constructs path programs from counterexamples and computes fixpoints for those path programs using abstract interpretation. If the fixpoints are strong enough to prove the path program to be correct, they are guaranteed to be loop invariants for the path program. If they are not strong enough, Ultimate Taipan uses an interpolating SMT solver to obtain state assertions from the original counterexample, thus guaranteeing progress.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

TACAS 2017 : 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 22. Apr. 2017 - 29. Apr. 2017, Uppsala
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690GREITSCHUS, Marius, Daniel DIETSCH, Matthias HEIZMANN, Alexander NUTZ, Claus SCHÄTZLE, Christian SCHILLING, Frank SCHÜSSELE, Andreas PODELSKI, 2017. Ultimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution). TACAS 2017 : 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Uppsala, 22. Apr. 2017 - 29. Apr. 2017. In: LEGAY, Axel, ed., Tiziana MARGARIA, ed.. Tools and algorithms for the construction and analysis of systems : 23rd international conference, TACAS 2017, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part 2. Berlin: Springer, 2017, pp. 399-403. Lecture Notes in Computer Science. 10206. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-54579-9. Available under: doi: 10.1007/978-3-662-54580-5_31
BibTex
@inproceedings{Greitschus2017Ultim-52704,
  year={2017},
  doi={10.1007/978-3-662-54580-5_31},
  title={Ultimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution)},
  number={10206},
  isbn={978-3-662-54579-9},
  issn={0302-9743},
  publisher={Springer},
  address={Berlin},
  series={Lecture Notes in Computer Science},
  booktitle={Tools and algorithms for the construction and analysis of systems : 23rd international conference, TACAS 2017, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part 2},
  pages={399--403},
  editor={Legay, Axel and Margaria, Tiziana},
  author={Greitschus, Marius and Dietsch, Daniel and Heizmann, Matthias and Nutz, Alexander and Schätzle, Claus and Schilling, Christian and Schüssele, Frank and Podelski, Andreas}
}
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/52704">
    <dc:creator>Heizmann, Matthias</dc:creator>
    <dcterms:abstract xml:lang="eng">Ultimate Taipan is a software model checker for C programs. It is based on a CEGAR variant, trace abstraction [7], where program abstractions, counterexample selection and abstraction refinement are based on automata. Ultimate Taipan constructs path programs from counterexamples and computes fixpoints for those path programs using abstract interpretation. If the fixpoints are strong enough to prove the path program to be correct, they are guaranteed to be loop invariants for the path program. If they are not strong enough, Ultimate Taipan uses an interpolating SMT solver to obtain state assertions from the original counterexample, thus guaranteeing progress.</dcterms:abstract>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52704"/>
    <dc:creator>Schüssele, Frank</dc:creator>
    <dc:creator>Nutz, Alexander</dc:creator>
    <dc:creator>Greitschus, Marius</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dc:contributor>Schätzle, Claus</dc:contributor>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-03T10:06:24Z</dc:date>
    <dc:contributor>Heizmann, Matthias</dc:contributor>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Schilling, Christian</dc:creator>
    <dc:contributor>Greitschus, Marius</dc:contributor>
    <dcterms:issued>2017</dcterms:issued>
    <dcterms:title>Ultimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution)</dcterms:title>
    <dc:language>eng</dc:language>
    <dc:creator>Podelski, Andreas</dc:creator>
    <dc:creator>Dietsch, Daniel</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>Schätzle, Claus</dc:creator>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Podelski, Andreas</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-03T10:06:24Z</dcterms:available>
    <dc:contributor>Nutz, Alexander</dc:contributor>
    <dc:contributor>Dietsch, Daniel</dc:contributor>
    <dc:contributor>Schüssele, Frank</dc:contributor>
    <dc:contributor>Schilling, Christian</dc:contributor>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen