Publikation: Broadening the applicability of local completeness analysis with intensional and extensional guarantees
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
Local Completeness Logic (LCL) is a proof system for program analysis rooted in abstract interpretation. The program semantics is under-approximated by any provable postcondition, like incorrectness logic does, but it is also over-approximated by a (locally) complete abstraction of such a postcondition, like Hoare logic does. Therefore, any derivable triple will either prove the program to be correct or unveil true bugs. While the completeness of a program's function with respect to an abstract domain is inherently extensional, LCL's rules demand the preservation of local completeness throughout the abstract interpreter's computations. This characteristic renders LCL analysis intensional, meaning it depends on the way the program is written. Consequently, LCL proof system may not derive all the valid triples. This paper addresses this discrepancy by: 1) designing new rules that allow one to perform part of the intensional analysis in different (complete) abstract domains whenever necessary; and 2) to compare their expressiveness. Notably, some of these new rules enable the derivation of all extensionally valid triples, thereby decoupling the set of provable properties from the way the program is written
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
ASCARI, Flavio, Roberto BRUNI, Roberta GORI, 2025. Broadening the applicability of local completeness analysis with intensional and extensional guarantees. In: Theoretical Computer Science. Elsevier. 2025, 1054, 115452. ISSN 0304-3975. eISSN 1879-2294. Verfügbar unter: doi: 10.1016/j.tcs.2025.115452BibTex
@article{Ascari2025-11Broad-74779,
title={Broadening the applicability of local completeness analysis with intensional and extensional guarantees},
year={2025},
doi={10.1016/j.tcs.2025.115452},
volume={1054},
issn={0304-3975},
journal={Theoretical Computer Science},
author={Ascari, Flavio and Bruni, Roberto and Gori, Roberta},
note={Article Number: 115452}
}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/74779">
<dc:contributor>Bruni, Roberto</dc:contributor>
<dc:contributor>Ascari, Flavio</dc:contributor>
<dcterms:issued>2025-11</dcterms:issued>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:abstract>Local Completeness Logic (LCL) is a proof system for program analysis rooted in abstract interpretation. The program semantics is under-approximated by any provable postcondition, like incorrectness logic does, but it is also over-approximated by a (locally) complete abstraction of such a postcondition, like Hoare logic does. Therefore, any derivable triple will either prove the program to be correct or unveil true bugs. While the completeness of a program's function with respect to an abstract domain is inherently extensional, LCL's rules demand the preservation of local completeness throughout the abstract interpreter's computations. This characteristic renders LCL analysis intensional, meaning it depends on the way the program is written. Consequently, LCL proof system may not derive all the valid triples. This paper addresses this discrepancy by: 1) designing new rules that allow one to perform part of the intensional analysis in different (complete) abstract domains whenever necessary; and 2) to compare their expressiveness. Notably, some of these new rules enable the derivation of all extensionally valid triples, thereby decoupling the set of provable properties from the way the program is written</dcterms:abstract>
<bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/74779"/>
<dc:creator>Gori, Roberta</dc:creator>
<dc:creator>Bruni, Roberto</dc:creator>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/74779/1/Ascari_2-1j74703xgp5l93.pdf"/>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2025-10-10T09:01:44Z</dc:date>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2025-10-10T09:01:44Z</dcterms:available>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:rights>Attribution-NonCommercial 4.0 International</dc:rights>
<dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc/4.0/"/>
<dcterms:title>Broadening the applicability of local completeness analysis with intensional and extensional guarantees</dcterms:title>
<dc:language>eng</dc:language>
<dc:contributor>Gori, Roberta</dc:contributor>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/74779/1/Ascari_2-1j74703xgp5l93.pdf"/>
<dc:creator>Ascari, Flavio</dc:creator>
</rdf:Description>
</rdf:RDF>
