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

Kurzanzeige
dc.contributor.authorGreitschus, Marius
dc.contributor.authorDietsch, Daniel
dc.contributor.authorHeizmann, Matthias
dc.contributor.authorNutz, Alexander
dc.contributor.authorSchätzle, Claus
dc.contributor.authorSchilling, Christian
dc.contributor.authorSchüssele, Frank
dc.contributor.authorPodelski, Andreas
dc.date.accessioned2021-02-03T10:06:24Z
dc.date.available2021-02-03T10:06:24Z
dc.date.issued2017eng
dc.description.abstractUltimate 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.eng
dc.description.versionpublishedeng
dc.identifier.doi10.1007/978-3-662-54580-5_31eng
dc.identifier.urihttps://kops.uni-konstanz.de/handle/123456789/52704
dc.language.isoengeng
dc.rightsterms-of-use
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/
dc.subject.ddc004eng
dc.titleUltimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution)eng
dc.typeINPROCEEDINGSeng
dspace.entity.typePublication
kops.citation.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}
}
kops.citation.iso690GREITSCHUS, 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_31deu
kops.citation.iso690GREITSCHUS, 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, Apr 22, 2017 - Apr 29, 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_31eng
kops.citation.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>
kops.conferencefieldTACAS 2017 : 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 22. Apr. 2017 - 29. Apr. 2017, Uppsaladeu
kops.date.conferenceEnd2017-04-29eng
kops.date.conferenceStart2017-04-22eng
kops.flag.knbibliographyfalse
kops.location.conferenceUppsalaeng
kops.sourcefieldLEGAY, Axel, ed., Tiziana MARGARIA, ed.. <i>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</i>. 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_31deu
kops.sourcefield.plainLEGAY, 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_31deu
kops.sourcefield.plainLEGAY, 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_31eng
kops.title.conferenceTACAS 2017 : 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systemseng
relation.isAuthorOfPublicationecb6e671-5807-41bc-bb31-f07a9b7a7c63
relation.isAuthorOfPublication.latestForDiscoveryecb6e671-5807-41bc-bb31-f07a9b7a7c63
source.bibliographicInfo.fromPage399eng
source.bibliographicInfo.seriesNumber10206eng
source.bibliographicInfo.toPage403eng
source.contributor.editorLegay, Axel
source.contributor.editorMargaria, Tiziana
source.identifier.eissn1611-3349eng
source.identifier.isbn978-3-662-54579-9eng
source.identifier.issn0302-9743eng
source.publisherSpringereng
source.publisher.locationBerlineng
source.relation.ispartofseriesLecture Notes in Computer Scienceeng
source.titleTools 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 2eng

Dateien

Sammlungen

Informatik und Informationswissenschaft: Publikationen