Minimization of Visibly Pushdown Automata Using Partial Max-SAT

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

HEIZMANN, Matthias, Christian SCHILLING, Daniel TISCHNER, 2017. Minimization of Visibly Pushdown Automata Using Partial Max-SAT. 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 1. Berlin:Springer, pp. 461-478. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-54576-8. Available under: doi: 10.1007/978-3-662-54577-5_27

@inproceedings{Heizmann2017Minim-52642, title={Minimization of Visibly Pushdown Automata Using Partial Max-SAT}, year={2017}, doi={10.1007/978-3-662-54577-5_27}, number={10205}, isbn={978-3-662-54576-8}, 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 1}, pages={461--478}, editor={Legay, Axel and Margaria, Tiziana}, author={Heizmann, Matthias and Schilling, Christian and Tischner, Daniel} }

<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/52642"> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:abstract xml:lang="eng">We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (Vpa). Vpa recognize a robust and algorithmically tractable fragment of context-free languages that is natural for modeling programs. We define an equivalence relation that is sufficient for language-preserving quotienting of Vpa. Our definition allows to merge states that have different behavior, as long as they show the same behavior for reachable equivalent stacks. We encode the existence of such a relation as a Boolean partial maximum satisfiability (PMax-Sat) problem and present an algorithm that quickly finds satisfying assignments. These assignments are sub-optimal solutions to the PMax-Sat problem but can still lead to a significant reduction of states. We integrated our method in the automata-based software verifier Ultimate Automizer and show performance improvements on benchmarks from the software verification competition SV-COMP.</dcterms:abstract> <dc:language>eng</dc:language> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:title>Minimization of Visibly Pushdown Automata Using Partial Max-SAT</dcterms:title> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:rights>terms-of-use</dc:rights> <dc:contributor>Schilling, Christian</dc:contributor> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-29T13:54:13Z</dc:date> <dcterms:issued>2017</dcterms:issued> <dc:contributor>Tischner, Daniel</dc:contributor> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-29T13:54:13Z</dcterms:available> <dc:creator>Schilling, Christian</dc:creator> <dc:contributor>Heizmann, Matthias</dc:contributor> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52642"/> <dc:creator>Heizmann, Matthias</dc:creator> <dc:creator>Tischner, Daniel</dc:creator> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account