Ultimate Automizer with SMTInterpol (Competition Contribution)

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

HEIZMANN, Matthias, Jürgen CHRIST, Daniel DIETSCH, Evren ERMIS, Jochen HOENICKE, Markus LINDENMANN, Alexander NUTZ, Christian SCHILLING, Andreas PODELSKI, 2013. Ultimate Automizer with SMTInterpol (Competition Contribution). TACAS 2013: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Rom, Mar 16, 2013 - Mar 24, 2013. In: PITERMAN, Nir, ed., Scott A. SMOLKA, ed.. Tools and algorithms for the construction and analysis of systems : 19th international conference, TACAS 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16 - 24, 2013 ; proceedings. Berlin:Springer, pp. 641-643. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-36741-0. Available under: doi: 10.1007/978-3-642-36742-7_53

@inproceedings{Heizmann2013Ultim-52569, title={Ultimate Automizer with SMTInterpol (Competition Contribution)}, year={2013}, doi={10.1007/978-3-642-36742-7_53}, number={7795}, isbn={978-3-642-36741-0}, issn={0302-9743}, address={Berlin}, publisher={Springer}, series={Lecture Notes in Computer Science}, booktitle={Tools and algorithms for the construction and analysis of systems : 19th international conference, TACAS 2013, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16 - 24, 2013 ; proceedings}, pages={641--643}, editor={Piterman, Nir and Smolka, Scott A.}, author={Heizmann, Matthias and Christ, Jürgen and Dietsch, Daniel and Ermis, Evren and Hoenicke, Jochen and Lindenmann, Markus and Nutz, Alexander and Schilling, Christian 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/52569"> <dc:contributor>Christ, Jürgen</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:contributor>Podelski, Andreas</dc:contributor> <dc:creator>Ermis, Evren</dc:creator> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dc:contributor>Schilling, Christian</dc:contributor> <dc:creator>Hoenicke, Jochen</dc:creator> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:creator>Heizmann, Matthias</dc:creator> <dcterms:title>Ultimate Automizer with SMTInterpol (Competition Contribution)</dcterms:title> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-26T14:10:52Z</dc:date> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Ermis, Evren</dc:contributor> <dc:contributor>Heizmann, Matthias</dc:contributor> <dc:contributor>Nutz, Alexander</dc:contributor> <dc:contributor>Hoenicke, Jochen</dc:contributor> <dc:creator>Schilling, Christian</dc:creator> <dcterms:issued>2013</dcterms:issued> <dc:creator>Lindenmann, Markus</dc:creator> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:rights>terms-of-use</dc:rights> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-26T14:10:52Z</dcterms:available> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52569"/> <dc:creator>Christ, Jürgen</dc:creator> <dc:creator>Podelski, Andreas</dc:creator> <dc:creator>Dietsch, Daniel</dc:creator> <dc:contributor>Dietsch, Daniel</dc:contributor> <dcterms:abstract xml:lang="eng">Ultimate Automizer is an automatic software verification tool for C programs. This tool is the first implementation of trace abstraction, which is an automata-theoretic approach to software verification. The implemented algorithm uses nested interpolants in its interprocedural program analysis. The interpolating SMT solver SMTInterpol is used to compute Craig interpolants.</dcterms:abstract> <dc:language>eng</dc:language> <dc:contributor>Lindenmann, Markus</dc:contributor> <dc:creator>Nutz, Alexander</dc:creator> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account