Keidel, Sven ; Helm, Dominik ; Roth, Tobias ; Mezini, Mira (2024)
A Modular Soundness Theory for the Blackboard Analysis Architecture.
33rd European Symposium on Programming (ESOP 2024). Luxembourg City, Luxembourg (06.04.2024 - 11.04.2024)
doi: 10.1007/978-3-031-57267-8_14
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
Sound static analyses are an important ingredient for compiler optimizations and program verification tools. However, mathematically proving that a static analysis is sound is a difficult task due to two problems. First, soundness proofs relate two complicated program semantics (the static and the dynamic semantics) which are hard to reason about. Second, the more the static and dynamic semantics differ, the more work a soundness proof needs to do to bridge the impedance mismatch. These problems increase the effort and complexity of soundness proofs. Existing soundness theories address these problems by deriving both the dynamic and static semantics from the same artifact, often called generic interpreter. A generic interpreter provides a common structure along which a soundness proof can be composed, which avoids having to reason about the analysis as a whole. However, a generic interpreter restricts which analyses can be derived, as all derived analyses must roughly follow the program execution order. To lift this restriction, we develop a soundness theory for the blackboard analysis architecture, which is capable of describing backward, demand-driven, and summary-based analyses. The architecture describes static analyses with small independent modules, which communicate via a central store. Soundness of a compound analysis follows from soundness of all of its modules. Furthermore, modules can be proven sound independently, even though modules depend on each other. We evaluate our theory by proving soundness of four analyses: a pointer and call-graph analysis, a reflection analysis, an immutability analysis, and a demand-driven reaching definitions analysis.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2024 |
| Autor(en): | Keidel, Sven ; Helm, Dominik ; Roth, Tobias ; Mezini, Mira |
| Art des Eintrags: | Bibliographie |
| Titel: | A Modular Soundness Theory for the Blackboard Analysis Architecture |
| Sprache: | Englisch |
| Publikationsjahr: | April 2024 |
| Verlag: | Springer |
| Buchtitel: | Programming Languages and Systems |
| Reihe: | Lecture Notes in Computer Science |
| Band einer Reihe: | 14577 |
| Veranstaltungstitel: | 33rd European Symposium on Programming (ESOP 2024) |
| Veranstaltungsort: | Luxembourg City, Luxembourg |
| Veranstaltungsdatum: | 06.04.2024 - 11.04.2024 |
| DOI: | 10.1007/978-3-031-57267-8_14 |
| URL / URN: | https://link.springer.com/chapter/10.1007/978-3-031-57267-8_... |
| Kurzbeschreibung (Abstract): | Sound static analyses are an important ingredient for compiler optimizations and program verification tools. However, mathematically proving that a static analysis is sound is a difficult task due to two problems. First, soundness proofs relate two complicated program semantics (the static and the dynamic semantics) which are hard to reason about. Second, the more the static and dynamic semantics differ, the more work a soundness proof needs to do to bridge the impedance mismatch. These problems increase the effort and complexity of soundness proofs. Existing soundness theories address these problems by deriving both the dynamic and static semantics from the same artifact, often called generic interpreter. A generic interpreter provides a common structure along which a soundness proof can be composed, which avoids having to reason about the analysis as a whole. However, a generic interpreter restricts which analyses can be derived, as all derived analyses must roughly follow the program execution order. To lift this restriction, we develop a soundness theory for the blackboard analysis architecture, which is capable of describing backward, demand-driven, and summary-based analyses. The architecture describes static analyses with small independent modules, which communicate via a central store. Soundness of a compound analysis follows from soundness of all of its modules. Furthermore, modules can be proven sound independently, even though modules depend on each other. We evaluate our theory by proving soundness of four analyses: a pointer and call-graph analysis, a reflection analysis, an immutability analysis, and a demand-driven reaching definitions analysis. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Softwaretechnik |
| Hinterlegungsdatum: | 03 Jun 2024 11:55 |
| Letzte Änderung: | 14 Okt 2024 12:52 |
| PPN: | 522200524 |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum