Publikation:

Proving hypersafety compositionally

Vorschaubild

Dateien

DOsualdo_2-1lvy4m2xpa5qp4.pdf
DOsualdo_2-1lvy4m2xpa5qp4.pdfGröße: 439.94 KBDownloads: 24

Datum

2022

Autor:innen

Farzan, Azadeh
Dreyer, Derek

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
http://nbn-resolving.de/urn:nbn:de:bsz:352-2-1lvy4m2xpa5qp4
DOI (zitierfähiger Link)
https://doi.org/10.1145/3563298
ArXiv-ID

Internationale Patentnummer

Link zur Lizenz
oops

Angaben zur Forschungsförderung

European Union (EU): 101003349

Projekt

Open Access-Veröffentlichung
Open Access Gold

Sammlungen

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

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published

Erschienen in

Proceedings of the ACM on Programming Languages. ACM. 2022, 6(OOPSLA2), S. 289-314. eISSN 2475-1421. Verfügbar unter: doi: 10.1145/3563298

Zusammenfassung

Hypersafety properties of arity N are program properties that relate N traces of a program (or, more generally, traces of N programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the N related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Hyperproperties, Modularity, Compositionality, Weakest Precondition

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690D'OSUALDO, Emanuele, Azadeh FARZAN, Derek DREYER, 2022. Proving hypersafety compositionally. In: Proceedings of the ACM on Programming Languages. ACM. 2022, 6(OOPSLA2), S. 289-314. eISSN 2475-1421. Verfügbar unter: doi: 10.1145/3563298
BibTex
@article{DOsualdo2022-10-31Provi-70863,
  year={2022},
  doi={10.1145/3563298},
  title={Proving hypersafety compositionally},
  number={OOPSLA2},
  volume={6},
  journal={Proceedings of the ACM on Programming Languages},
  pages={289--314},
  author={D'Osualdo, Emanuele and Farzan, Azadeh and Dreyer, Derek}
}
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/70863">
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-09-30T07:51:40Z</dc:date>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/70863"/>
    <dc:creator>Farzan, Azadeh</dc:creator>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:abstract>Hypersafety properties of arity N are program properties that relate N traces of a program (or, more generally, traces of N programs). 
Classic examples include determinism, idempotence, and associativity. 
A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the N related programs. 
We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. 
We prove LHC sound and apply it to a number of challenging examples.</dcterms:abstract>
    <dc:contributor>Dreyer, Derek</dc:contributor>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/70863/1/DOsualdo_2-1lvy4m2xpa5qp4.pdf"/>
    <dcterms:issued>2022-10-31</dcterms:issued>
    <dc:creator>D'Osualdo, Emanuele</dc:creator>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/70863/1/DOsualdo_2-1lvy4m2xpa5qp4.pdf"/>
    <dc:contributor>D'Osualdo, Emanuele</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2024-09-30T07:51:40Z</dcterms:available>
    <dc:creator>Dreyer, Derek</dc:creator>
    <dc:contributor>Farzan, Azadeh</dc:contributor>
    <dcterms:title>Proving hypersafety compositionally</dcterms:title>
    <dc:language>eng</dc:language>
  </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
Unbekannt
Diese Publikation teilen