KOPS - The Institutional Repository of the University of Konstanz

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

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

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

GREITSCHUS, 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, pp. 399-403. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-54579-9. Available under: doi: 10.1007/978-3-662-54580-5_31

@inproceedings{Greitschus2017Ultim-52704, title={Ultimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution)}, year={2017}, doi={10.1007/978-3-662-54580-5_31}, number={10206}, isbn={978-3-662-54579-9}, issn={0302-9743}, address={Berlin}, publisher={Springer}, 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 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/rdf/resource/123456789/52704"> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Schätzle, Claus</dc:contributor> <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> <dc:creator>Schilling, Christian</dc:creator> <dc:creator>Nutz, Alexander</dc:creator> <dc:language>eng</dc:language> <dc:contributor>Heizmann, Matthias</dc:contributor> <dc:contributor>Dietsch, Daniel</dc:contributor> <dcterms:issued>2017</dcterms:issued> <dc:creator>Schätzle, Claus</dc:creator> <dc:creator>Greitschus, Marius</dc:creator> <dc:contributor>Schilling, Christian</dc:contributor> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Schüssele, Frank</dc:contributor> <dc:creator>Schüssele, Frank</dc:creator> <dc:contributor>Podelski, Andreas</dc:contributor> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-03T10:06:24Z</dcterms:available> <dc:contributor>Nutz, Alexander</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:rights>terms-of-use</dc:rights> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-02-03T10:06:24Z</dc:date> <dc:creator>Heizmann, Matthias</dc:creator> <dc:contributor>Greitschus, Marius</dc:contributor> <dcterms:title>Ultimate Taipan : Trace Abstraction and Abstract Interpretation (Competition Contribution)</dcterms:title> <dc:creator>Dietsch, Daniel</dc:creator> <dc:creator>Podelski, Andreas</dc:creator> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52704"/> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account