Publikation:

Automatic Verification of Erlang-Style Concurrency

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2013

Autor:innen

Kochems, Jonathan
Ong, C. -H. Luke

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-642-38856-9_24
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

LOGOZZO, Francesco, Hrsg., Manuel FÄHNDRICH, Hrsg.. Static Analysis : 20th International Symposium, SAS 2013, Proceedings. Berlin: Springer, 2013, S. 454-476. Lecture Notes in Computer Science (LNCS). 7935. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-38855-2. Verfügbar unter: doi: 10.1007/978-3-642-38856-9_24

Zusammenfassung

This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce λ Actor, a prototypical functional language with pattern-matching algebraic data types, augmented with process creation and asynchronous message-passing primitives. We formalise an abstract model of λ Actor programs called Actor Communicating System (ACS) which has a natural interpretation as a vector addition system, for which some verification problems are decidable. We give a parametric abstract interpretation framework for λ Actor and use it to build a polytime computable, flow-based, abstract semantics of λ Actor programs, which we then use to bootstrap the ACS construction, thus deriving a more accurate abstract model of the input program.

We evaluate the method which we implemented in the prototype Soter. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties. Though the ACS coverability problem is Expspace-complete, Soter can analyse non-trivial programs in a matter of seconds.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Erlang, Infinite-state Systems Verification, Petri Nets

Konferenz

Static Analysis : 20th International Symposium, SAS 2013, 20. Juni 2013 - 22. Juni 2013, Seattle, WA, USA
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690D'OSUALDO, Emanuele, Jonathan KOCHEMS, C. -H. Luke ONG, 2013. Automatic Verification of Erlang-Style Concurrency. Static Analysis : 20th International Symposium, SAS 2013. Seattle, WA, USA, 20. Juni 2013 - 22. Juni 2013. In: LOGOZZO, Francesco, Hrsg., Manuel FÄHNDRICH, Hrsg.. Static Analysis : 20th International Symposium, SAS 2013, Proceedings. Berlin: Springer, 2013, S. 454-476. Lecture Notes in Computer Science (LNCS). 7935. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-642-38855-2. Verfügbar unter: doi: 10.1007/978-3-642-38856-9_24
BibTex
@inproceedings{DOsualdo2013Autom-71001,
  year={2013},
  doi={10.1007/978-3-642-38856-9_24},
  title={Automatic Verification of Erlang-Style Concurrency},
  number={7935},
  isbn={978-3-642-38855-2},
  issn={0302-9743},
  publisher={Springer},
  address={Berlin},
  series={Lecture Notes in Computer Science (LNCS)},
  booktitle={Static Analysis : 20th International Symposium, SAS 2013, Proceedings},
  pages={454--476},
  editor={Logozzo, Francesco and Fähndrich, Manuel},
  author={D'Osualdo, Emanuele and Kochems, Jonathan and Ong, C. -H. Luke}
}
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/71001">
    <dc:contributor>D'Osualdo, Emanuele</dc:contributor>
    <dc:creator>Ong, C. -H. Luke</dc:creator>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:abstract>This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce λ Actor, a prototypical functional language with pattern-matching algebraic data types, augmented with process creation and asynchronous message-passing primitives. We formalise an abstract model of λ Actor programs called Actor Communicating System (ACS) which has a natural interpretation as a vector addition system, for which some verification problems are decidable. We give a parametric abstract interpretation framework for λ Actor and use it to build a polytime computable, flow-based, abstract semantics of λ Actor programs, which we then use to bootstrap the ACS construction, thus deriving a more accurate abstract model of the input program.

We evaluate the method which we implemented in the prototype Soter. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties. Though the ACS coverability problem is Expspace-complete, Soter can analyse non-trivial programs in a matter of seconds.</dcterms:abstract>
    <dc:creator>Kochems, Jonathan</dc:creator>
    <dc:contributor>Kochems, Jonathan</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:10:36Z</dcterms:available>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-10-18T07:10:36Z</dc:date>
    <dc:creator>D'Osualdo, Emanuele</dc:creator>
    <dc:language>eng</dc:language>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/71001"/>
    <dcterms:issued>2013</dcterms:issued>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:title>Automatic Verification of Erlang-Style Concurrency</dcterms:title>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Ong, C. -H. Luke</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