Publikation:

Logics for Extensional, Locally Complete Analysis via Domain Refinements

Vorschaubild

Dateien

Ascari_2-fe9tx0nb7ivh8.pdf
Ascari_2-fe9tx0nb7ivh8.pdfGröße: 364.13 KBDownloads: 3

Datum

2023

Autor:innen

Bruni, Roberto
Gori, Roberta

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-fe9tx0nb7ivh8
DOI (zitierfähiger Link)
https://doi.org/10.1007/978-3-031-30044-8_1
ArXiv-ID

Internationale Patentnummer

Link zur Lizenz

CC BY 4.0

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Bookpart

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

WIES, Thomas, Hrsg.. Programming Languages and Systems : 32nd European Symposium on Programming, ESOP 2023, Proceedings. Cham: Springer, 2023, S. 1-27. Lecture Notes in Computer Science (LNCS). 13990. ISBN 978-3-031-30043-1. Verfügbar unter: doi: 10.1007/978-3-031-30044-8_1

Zusammenfassung

Abstract interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness Logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple ⊢A [P] c [Q] in the logic implies completeness of an intensional abstraction of program c on input P and is such that Q can be used to decide (in)correctness. However, completeness itself is an extensional property of the function computed by the program, while the above intensional analysis depends on the way the program is written and therefore not all valid triples can be derived in the proof system. Our main contribution is the study of new inference rules which allow one to perform part of the intensional analysis in a more precise abstract domain, and then to transfer the result back to the coarser domain. With these new rules, all (extensionally) valid triples can be derived in the proof system, thus untying the set of provable properties from the way the program is written.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Abstract interpretation, Completeness in abstract interpre- tation, Hoare logic, Abstract domain refinement, Extensionality

Konferenz

Programming Languages and Systems : 32nd European Symposium on Programming, ESOP 2023, 22. Apr. 2023 - 27. Apr. 2023, Paris, France
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690ASCARI, Flavio, Roberto BRUNI, Roberta GORI, 2023. Logics for Extensional, Locally Complete Analysis via Domain Refinements. Programming Languages and Systems : 32nd European Symposium on Programming, ESOP 2023. Paris, France, 22. Apr. 2023 - 27. Apr. 2023. In: WIES, Thomas, Hrsg.. Programming Languages and Systems : 32nd European Symposium on Programming, ESOP 2023, Proceedings. Cham: Springer, 2023, S. 1-27. Lecture Notes in Computer Science (LNCS). 13990. ISBN 978-3-031-30043-1. Verfügbar unter: doi: 10.1007/978-3-031-30044-8_1
BibTex
@inproceedings{Ascari2023-04Logic-76130,
  title={Logics for Extensional, Locally Complete Analysis via Domain Refinements},
  year={2023},
  doi={10.1007/978-3-031-30044-8_1},
  number={13990},
  isbn={978-3-031-30043-1},
  address={Cham},
  publisher={Springer},
  series={Lecture Notes in Computer Science (LNCS)},
  booktitle={Programming Languages and Systems : 32nd European Symposium on Programming, ESOP 2023, Proceedings},
  pages={1--27},
  editor={Wies, Thomas},
  author={Ascari, Flavio and Bruni, Roberto and Gori, Roberta}
}
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/76130">
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2026-02-05T13:27:46Z</dcterms:available>
    <dc:contributor>Bruni, Roberto</dc:contributor>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/76130/1/Ascari_2-fe9tx0nb7ivh8.pdf"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2026-02-05T13:27:46Z</dc:date>
    <dc:contributor>Ascari, Flavio</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/76130/1/Ascari_2-fe9tx0nb7ivh8.pdf"/>
    <dc:creator>Ascari, Flavio</dc:creator>
    <dc:rights>Attribution 4.0 International</dc:rights>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:title>Logics for Extensional, Locally Complete Analysis via Domain Refinements</dcterms:title>
    <dc:language>eng</dc:language>
    <dc:creator>Gori, Roberta</dc:creator>
    <dc:contributor>Gori, Roberta</dc:contributor>
    <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by/4.0/"/>
    <dcterms:issued>2023-04</dcterms:issued>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/76130"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:abstract>Abstract interpretation is a framework to design sound static analyses by over-approximating the set of program behaviours. While over-approximations can prove correctness, they cannot witness incorrectness because false alarms may arise. An ideal, but uncommon, situation is completeness of the abstraction that can ensure no false alarm is introduced by the abstract interpreter. Local Completeness Logic is a proof system that can decide both correctness and incorrectness of a program: any provable triple ⊢A [P] c [Q] in the logic implies completeness of an intensional abstraction of program c on input P and is such that Q can be used to decide (in)correctness. However, completeness itself is an extensional property of the function computed by the program, while the above intensional analysis depends on the way the program is written and therefore not all valid triples can be derived in the proof system. Our main contribution is the study of new inference rules which allow one to perform part of the intensional analysis in a more precise abstract domain, and then to transfer the result back to the coarser domain. With these new rules, all (extensionally) valid triples can be derived in the proof system, thus untying the set of provable properties from the way the program is written.</dcterms:abstract>
    <dc:creator>Bruni, Roberto</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
  </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