Type of Publication: | Contribution to a conference collection |
Publication status: | Published |
Author: | Heizmann, Matthias; Christ, Jürgen; Dietsch, Daniel; Hoenicke, Jochen; Lindenmann, Markus; Musa, Betim; Schilling, Christian; Wissert, Stefan; Podelski, Andreas |
Year of publication: | 2014 |
Conference: | TACAS 2014: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 5, 2014 - Apr 13, 2014, Grenoble |
Published in: | Tools and algorithms for the construction and analysis of systems : 20th International Conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014 ; proceedings / Ábrahám, Erika; Havelund, Klaus (ed.). - Berlin : Springer, 2014. - (Lecture Notes in Computer Science ; 8413). - pp. 418-420. - ISSN 0302-9743. - eISSN 1611-3349. - ISBN 978-3-642-54861-1 |
DOI (citable link): | https://dx.doi.org/10.1007/978-3-642-54862-8_35 |
Summary: |
Ultimate Automizer is an automatic software verification tool for C programs. This tool is a prototype implementation of an automata-theoretic approach that allows a modular verification of programs. Furthermore, this is the first implementation of a novel interpolation technique where interpolants are not obtained from an interpolating theorem prover but from a combination of a live variable analysis, interprocedural predicate transformers and unsatisfiable cores.
|
Subject (DDC): | 004 Computer Science |
Keywords: | Graph Reachability, Demonstration Category, Predicate Transformer, Software Model Check, Unsatisfiable Core |
Files | Size | Format | View |
---|---|---|---|
There are no files associated with this item. |
HEIZMANN, Matthias, Jürgen CHRIST, Daniel DIETSCH, Jochen HOENICKE, Markus LINDENMANN, Betim MUSA, Christian SCHILLING, Stefan WISSERT, Andreas PODELSKI, 2014. Ultimate Automizer with Unsatisfiable Cores (Competition Contribution). TACAS 2014: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Grenoble, Apr 5, 2014 - Apr 13, 2014. In: ÁBRAHÁM, Erika, ed., Klaus HAVELUND, ed.. Tools and algorithms for the construction and analysis of systems : 20th International Conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014 ; proceedings. Berlin:Springer, pp. 418-420. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-54861-1. Available under: doi: 10.1007/978-3-642-54862-8_35
@inproceedings{Heizmann2014Ultim-52570, title={Ultimate Automizer with Unsatisfiable Cores (Competition Contribution)}, year={2014}, doi={10.1007/978-3-642-54862-8_35}, number={8413}, isbn={978-3-642-54861-1}, issn={0302-9743}, address={Berlin}, publisher={Springer}, series={Lecture Notes in Computer Science}, booktitle={Tools and algorithms for the construction and analysis of systems : 20th International Conference, TACAS 2014, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014 ; proceedings}, pages={418--420}, editor={Ábrahám, Erika and Havelund, Klaus}, author={Heizmann, Matthias and Christ, Jürgen and Dietsch, Daniel and Hoenicke, Jochen and Lindenmann, Markus and Musa, Betim and Schilling, Christian and Wissert, Stefan 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/52570"> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-26T14:25:00Z</dcterms:available> <dc:rights>terms-of-use</dc:rights> <dc:creator>Lindenmann, Markus</dc:creator> <dc:contributor>Schilling, Christian</dc:contributor> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Wissert, Stefan</dc:contributor> <dc:creator>Musa, Betim</dc:creator> <dcterms:abstract xml:lang="eng">Ultimate Automizer is an automatic software verification tool for C programs. This tool is a prototype implementation of an automata-theoretic approach that allows a modular verification of programs. Furthermore, this is the first implementation of a novel interpolation technique where interpolants are not obtained from an interpolating theorem prover but from a combination of a live variable analysis, interprocedural predicate transformers and unsatisfiable cores.</dcterms:abstract> <dc:contributor>Podelski, Andreas</dc:contributor> <dc:contributor>Lindenmann, Markus</dc:contributor> <dcterms:title>Ultimate Automizer with Unsatisfiable Cores (Competition Contribution)</dcterms:title> <dc:contributor>Dietsch, Daniel</dc:contributor> <dc:creator>Dietsch, Daniel</dc:creator> <dc:creator>Heizmann, Matthias</dc:creator> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:contributor>Heizmann, Matthias</dc:contributor> <dc:creator>Podelski, Andreas</dc:creator> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52570"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Christ, Jürgen</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Hoenicke, Jochen</dc:contributor> <dc:contributor>Musa, Betim</dc:contributor> <dc:creator>Schilling, Christian</dc:creator> <dc:language>eng</dc:language> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-26T14:25:00Z</dc:date> <dc:creator>Wissert, Stefan</dc:creator> <dc:creator>Hoenicke, Jochen</dc:creator> <dcterms:issued>2014</dcterms:issued> <dc:creator>Christ, Jürgen</dc:creator> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> </rdf:Description> </rdf:RDF>