Automatische Analyse nebenläufiger Pointerprogramme
Theoretische Informatik
Zusammenfassung der Projektergebnisse
Throughout the funding period of the ATTESTOR project, our work on formal methods for pointermanipulating programs has advanced the state-of-the-art in several aspects. We developed a deeper understanding of the connection between state-space abstraction based on graph rewriting and symbolic representation of program states through graph grammars and separation logic, respectively. This allows recasting language inclusion as logical entailment and vice versa. In particular, exploiting the aforementioned relationship led to novel decision procedures for large fragments of symbolic heap separation logic. Furthermore, we considered extensions of graph grammars beyond context-freeness that enable reasoning about intricate shape-numeric properties such as balancedness. The applicability of our methods was demonstrated by an implementation supporting the verification of both basic memory safety and advanced functional properties of Java pointer programs. In the case of property violations, it provides valuable feedback to the user in the form of realisable counterexamples and concrete inputs allowing to reproduce the underlying issue. Moreover, we were able to develop a basic framework for thread-modular heap abstraction and analysis of concurrent pointer programs using the concept of permissions. However, our original goals regarding a more adaptive handling of permissions and the support for more advanced synchronisation mechanisms have not been fully accomplished. One reason was that the amount of information that is required to ensure a sufficient degree of precision in the permission information grows abundantly. Another reason was the increasing interest in probabilistic programs and particularly randomised algorithms manipulating dynamic data structures. We developed a quantitative separation logic (QSL) which conservatively extends separation logic to enable quantitative reasoning about probabilistic pointer programs at source-code level. For example, QSL has been successfully applied to verify shuffling algorithms and a simplified version of the melding procedure of randomised meldable heaps. This logic, which allows to reason about numerical values such as the expected (or average) size of data structures, should most likely be considered as the most notable theoretical result of our project. It initiated a promising strand of research that attracted much interest in the community, as witnessed by other recently published works.
Projektbezogene Publikationen (Auswahl)
- Unified reasoning about robustness properties of symbolic-heap separation logic. In ESOP 2017, volume 10201 of LNCS, pages 611–638. Springer, 2017
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger
(Siehe online unter https://doi.org/10.1007/978-3-662-54434-1_23) - Graph-based shape analysis beyond context-freeness. In Proc. 16th Int. Conf. on Software Engineering and Formal Methods (SEFM 2018), volume 10886 of LNCS, pages 271–286. Springer, 2018
Hannah Arndt, Christina Jansen, Christoph Matheja, and Thomas Noll
(Siehe online unter https://doi.org/10.1007/978-3-319-92970-5_17) - Let this graph be your witness! An attestor for verifying Java pointer programs. In Proc. CAV 2018, Part II, volume 10982 of LNCS, pages 3–11. Springer, 2018
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(Siehe online unter https://doi.org/10.1007/978-3-319-96142-2_1) - Effective entailment checking for separation logic with inductive definitions. In TACAS, volume 11428 of LNCS, pages 319–336. Springer, 2019
Jens Katelaan, Christoph Matheja, and Florian Zuleger
(Siehe online unter https://doi.org/10.1007/978-3-030-17465-1_18) - Quantitative separation logic. Proceedings of the ACM on Programming Languages, 3(POPL):34:1– 34:29, January 2019
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll
(Siehe online unter https://doi.org/10.1145/3290347) - SL-COMP: Competition of solvers for separation logic. In TACAS 2019, volume 11429 of LNCS, pages 116–132. Springer, 2019
Mihaela Sighireanu, Juan A. Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, Andrew Reynolds, Cristina Serban, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger, Wei-Ngan Chin, Quang Loc Le, Quang-Trung Ta, Ton-Chanh Le, Thanh-Toan Nguyen, Siau-Cheng Khoo, Michal Cyprian, Adam Rogalewicz, Tomas Vojnar, Constantin Enea, Ondrej Lengal, Chong Gao, and Zhilin Wu
(Siehe online unter https://doi.org/10.1007/978-3-030-17502-3_8)
