Publikation:

Minimization of Visibly Pushdown Automata Using Partial Max-SAT

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2017

Autor:innen

Heizmann, Matthias
Tischner, Daniel

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
DOI (zitierfähiger Link)
https://doi.org/10.1007/978-3-662-54577-5_27
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen 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, 2017, pp. 461-478. Lecture Notes in Computer Science. 10205. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-54576-8. Available under: doi: 10.1007/978-3-662-54577-5_27

Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

TACAS 2017 : 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 22. Apr. 2017 - 29. Apr. 2017, Uppsala
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690HEIZMANN, 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, 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 1. Berlin: Springer, 2017, pp. 461-478. Lecture Notes in Computer Science. 10205. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-54576-8. Available under: doi: 10.1007/978-3-662-54577-5_27
BibTex
@inproceedings{Heizmann2017Minim-52642,
  year={2017},
  doi={10.1007/978-3-662-54577-5_27},
  title={Minimization of Visibly Pushdown Automata Using Partial Max-SAT},
  number={10205},
  isbn={978-3-662-54576-8},
  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 1},
  pages={461--478},
  editor={Legay, Axel and Margaria, Tiziana},
  author={Heizmann, Matthias and Schilling, Christian and Tischner, Daniel}
}
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/52642">
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-29T13:54:13Z</dc:date>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/52642"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Schilling, Christian</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-01-29T13:54:13Z</dcterms:available>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Tischner, Daniel</dc:contributor>
    <dcterms:title>Minimization of Visibly Pushdown Automata Using Partial Max-SAT</dcterms:title>
    <dc:creator>Tischner, Daniel</dc:creator>
    <dcterms:issued>2017</dcterms:issued>
    <dc:creator>Heizmann, Matthias</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <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>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Schilling, Christian</dc:creator>
    <dc:language>eng</dc:language>
    <dc:contributor>Heizmann, Matthias</dc:contributor>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen