A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. (English) Zbl 07650597
References:
| [1] | Antonopoulos, Timos, Gorogiannis, Nikos, Haase, Christoph, Kanovich, Max I., and Ouaknine, Joël. 2014. Foundations for decision problems in separation logic with general inductive predicates. In Proceedings of FOSSACS’14. 411-425. · Zbl 1406.03046 |
| [2] | Appel, Andrew W.. 2014. Program Logics—For Certified Compilers. Cambridge University Press. · Zbl 1298.68009 |
| [3] | Bar-Hillel, Yehoshua, Perles, Micha, and Shamir, Eli. 1961. On formal properties of simple phrase structure grammars. Sprachtypologie und Universalienforschung14 (1961), 143-172. · Zbl 0106.34501 |
| [4] | Batz, Kevin, Kaminski, Benjamin Lucien, Katoen, Joost-Pieter, Matheja, Christoph, and Noll, Thomas. 2019. Quantitative separation logic: A logic for reasoning about probabilistic pointer programs. Proceedings of the ACM on Programming Languages3, POPL (2019), Article 34, 29 pages. |
| [5] | Berdine, Josh, Calcagno, Cristiano, Cook, Byron, Distefano, Dino, O’Hearn, Peter W., Wies, Thomas, and Yang, Hongseok. 2007. Shape analysis for composite data structures. In Proceedings of CAV’07. 178-192. · Zbl 1135.68372 |
| [6] | Berdine, Josh, Calcagno, Cristiano, and O’Hearn, Peter W.. 2004. A decidable fragment of separation logic. In Proceedings of FSTTCS’04. 97-109. · Zbl 1117.03337 |
| [7] | Berdine, Josh, Calcagno, Cristiano, and O’Hearn, Peter W.. 2005a. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of FMCO’05. 115-137. |
| [8] | Berdine, Josh, Calcagno, Cristiano, and O’Hearn, Peter W.. 2005b. Symbolic execution with separation logic. In Proceedings of APLAS’05. 52-68. · Zbl 1159.68363 |
| [9] | Berdine, Josh, Cook, Byron, and Ishtiaq, Samin. 2011. SLAyer: Memory safety for systems-level code. In Proceedings of CAV’11. 178-183. |
| [10] | Blom, Stefan and Huisman, Marieke. 2015. Witnessing the elimination of magic wands. International Journal on Software Tools for Technology Transfer17, 6 (2015), 757-781. |
| [11] | Brochenin, Rémi, Demri, Stéphane, and Lozes, Étienne. 2012. On the almighty wand. Information and Computation211 (2012), 106-137. · Zbl 1262.03051 |
| [12] | Brotherston, James. 2007. Formalised inductive reasoning in the logic of bunched implications. In Static Analysis. Lecture Notes in Computer Science, Vol. 4634. Springer, 87-103. · Zbl 1211.68081 |
| [13] | Brotherston, James, Distefano, Dino, and Petersen, Rasmus Lerche dahl. 2011. Automated cyclic entailment proofs in separation logic. In Proceedings of CADE’11. 131-146. · Zbl 1341.68184 |
| [14] | Brotherston, James, Fuhs, Carsten, Pérez, Juan Antonio Navarro, and Gorogiannis, Nikos. 2014. A decision procedure for satisfiability in separation logic with inductive predicates. In Proceedings of CSL-LICS’14. Article 25, 10 pages. · Zbl 1401.68111 |
| [15] | Calcagno, Cristiano and Distefano, Dino. 2011. Infer: An automatic program verifier for memory safety of C programs. In Proceedings of NFM’11. 459-465. |
| [16] | Calcagno, Cristiano, Distefano, Dino, Dubreil, Jérémy, Gabi, Dominik, Hooimeijer, Pieter, Luca, Martino, O’Hearn, Peter W., Papakonstantinou, Irene, Purbrick, Jim, and Rodriguez, Dul ma. 2015. Moving fast with software verification. In Proceedings of NFM’15. 3-11. |
| [17] | Calcagno, Cristiano, Distefano, Dino, O’Hearn, Peter W., and Yang, Hongseok. 2006. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In Proceedings of SAS’06. 182-203. · Zbl 1225.68069 |
| [18] | Calcagno, Cristiano, Distefano, Dino, O’Hearn, Peter W., and Yang, Hongseok. 2011. Compositional shape analysis by means of bi-abduction. Journal of the ACM58, 6 (2011), Article 26, 66 pages. · Zbl 1281.68155 |
| [19] | Calcagno, Cristiano, O’Hearn, Peter W., and Yang, Hongseok. 2007. Local action and abstract separation logic. In Proceedings of LICS’07. 366-378. |
| [20] | Calcagno, Cristiano, Yang, Hongseok, and O’Hearn, Peter W.. 2001. Computability and complexity results for a spatial assertion language for data structures. In Proceedings of APLAS’01. 289-300. · Zbl 1052.68590 |
| [21] | Chin, Wei-Ngan, David, Cristina, Nguyen, Huu Hai, and Qin, Shengchao. 2012. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming77, 9 (2012), 1006-1036. · Zbl 1243.68148 |
| [22] | Cook, Byron, Haase, Christoph, Ouaknine, Joël, Parkinson, Matthew J., and Worrell, James. 2011. Tractable reasoning in a fragment of separation logic. In Proceedings of CONCUR’11. 235-249. · Zbl 1300.03017 |
| [23] | Courcelle, Bruno and Engelfriet, Joost. 2012. Graph Structure and Monadic Second-Order Logic—A Language-Theoretic Approach. , Vol. 138. Cambridge University Press. · Zbl 1257.68006 |
| [24] | Cousot, Patrick and Cousot, Radhia. 1979. Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics82, 1 (1979), 43-57. · Zbl 0413.06004 |
| [25] | Diestel, Reinhard. 2016. Graph Theory (5th ed.). Graduate Texts in Mathematics, Vol. 173. Springer. |
| [26] | Echenim, Mnacho, Iosif, Radu, and Peltier, Nicolas. 2020a. The Bernays-Schönfinkel-Ramsey class of separation logic with uninterpreted predicates. ACM Transactions on Computational Logic21, 3 (2020), Article 19, 46 pages. · Zbl 1446.03064 |
| [27] | Echenim, Mnacho, Iosif, Radu, and Peltier, Nicolas. 2020b. Entailment checking in separation logic with inductive definitions is 2-EXPTIME hard. In Proceedings of LPAR’20. 191-211. |
| [28] | Echenim, Mnacho, Iosif, Radu, and Peltier, Nicolas. 2021. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In Proceedings of CSL’21. · Zbl 1541.03105 |
| [29] | Enea, Constantin, Lengál, Ondrej, Sighireanu, Mihaela, and Vojnar, Tomás. 2017. SPEN: A solver for separation logic. In Proceedings of NFM’17. 302-309. |
| [30] | Gotsman, Alexey, Berdine, Josh, Cook, Byron, and Sagiv, Mooly. 2007. Thread-modular shape analysis. In Proceedings of PLDI’07. 266-277. |
| [31] | Hopcroft, John E., Motwani, Rajeev, and Ullman, Jeffrey D.. 2007. Introduction to Automata Theory, Languages, and Computation (3rd ed.). Addison-Wesley. · Zbl 0980.68066 |
| [32] | Iosif, Radu, Rogalewicz, Adam, and Simácek, Jirí. 2013. The tree width of separation logic with recursive definitions. In Proceedings of CADE’13. 21-38. · Zbl 1329.03068 |
| [33] | Iosif, Radu, Rogalewicz, Adam, and Vojnar, Tomás. 2014. Deciding entailments in inductive separation logic with tree automata. In Proceedings of ATVA’14. 201-218. · Zbl 1448.68266 |
| [34] | Ishtiaq, Samin S. and O’Hearn, Peter W.. 2001. BI as an assertion language for mutable data structures. In Proceedings of POPL’01. 14-26. · Zbl 1323.68077 |
| [35] | Jacobs, Bart, Smans, Jan, Philippaerts, Pieter, Vogels, Frédéric, Penninckx, Willem, and Piessens, Frank. 2011. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of NFM’11. 41-55. |
| [36] | Jansen, Christina, Katelaan, Jens, Matheja, Christoph, Noll, Thomas, and Zuleger, Florian. 2017. Unified reasoning about robustness properties of symbolic-heap separation logic. In Proceedings of ESOP’17. 611-638. · Zbl 1485.68068 |
| [37] | Jung, Ralf, Krebbers, Robbert, Jourdan, Jacques-Henri, Bizjak, Ales, Birkedal, Lars, and Dreyer, Derek. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming28 (2018), e20. · Zbl 1476.68062 |
| [38] | Katelaan, Jens, Matheja, Christoph, and Zuleger, Florian. 2019. Effective entailment checking for separation logic with inductive definitions. In Proceedings of TACAS’19. 319-336. · Zbl 1527.68131 |
| [39] | Katelaan, Jens and Zuleger, Florian. 2020. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In Proceedings of LPAR’20. 390-408. |
| [40] | Le, Quang Loc, Tatsuta, Makoto, Sun, Jun, and Chin, Wei-Ngan. 2017. A decidable fragment in separation logic with inductive predicates and arithmetic. In Proceedings of CAV’17. 495-517. · Zbl 1497.03048 |
| [41] | Matheja, Christoph. 2020. Automated Reasoning and Randomization in Separation Logic. Ph.D. Dissertation. RWTH Aachen University. |
| [42] | Müller, Peter, Schwerhoff, Malte, and Summers, Alexander J.. 2017. Viper: A verification infrastructure for permission-based reasoning. In Dependable Software Systems Engineering. IOS Press, 104-125. · Zbl 1475.68191 |
| [43] | Pagel, Jens, Matheja, Christoph, and Zuleger, Florian. 2020. Complete entailment checking for separation logic with inductive definitions. CoRRabs/2002.01202 (2020). |
| [44] | Piskac, Ruzica, Wies, Thomas, and Zufferey, Damien. 2013. Automating separation logic using SMT. In Proceedings of CAV’13. 773-789. |
| [45] | Piskac, Ruzica, Wies, Thomas, and Zufferey, Damien. 2014a. GRASShopper—Complete heap verification with mixed specifications. In Proceedings of TACAS’14. 124-139. |
| [46] | Piskac, Ruzica, Wies, Thomas, and Zufferey, Damien. 2014b. Automating separation logic with trees and data. In Proceedings of CAV’14. 711-728. |
| [47] | Reynolds, John C.. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of LICS’02. 55-74. |
| [48] | Schwerhoff, Malte and Summers, Alexander J.. 2015. Lightweight support for magic wands in an automatic verifier. In Proceedings of ECOOP’15. 614-638. |
| [49] | Sighireanu, Mihaela, Navarro Perez, Juan A., Rybalchenko, Andrey, Gorogiannis, Nikos, Iosif, Radu, Reynolds, Andrew, Serban, Cristina, et al.2019. SL-COMP: Competition of solvers for separation logic. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 11429. Springer, 116-132. |
| [50] | Ta, Quang-Trung, Le, Ton Chanh, Khoo, Siau-Cheng, and Chin, Wei-Ngan. 2016. Automated mutual explicit induction proof in separation logic. In Formal Methods. Lecture Notes in Computer Science, Vol. 9995. Springer, 659-676. · Zbl 1427.68350 |
| [51] | Ta, Quang-Trung, Le, Ton Chanh, Khoo, Siau-Cheng, and Chin, Wei-Ngan. 2018. Automated lemma synthesis in symbolic-heap separation logic. Proceedings of the ACM on Programming Languages2, POPL (2018), Article 9, 29 pages. · Zbl 1425.68382 |
| [52] | Thakur, Aditya V., Breck, Jason, and Reps, Thomas W.. 2014. Satisfiability modulo abstraction for separation logic with linked lists. In Proceedings of SPIN’14. 58-67. |
| [53] | Yang, Hongseok. 2001. Local Reasoning for Stateful Programs. . University of Illinois at Urbana-Champaign, Champaign, IL. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
