Heap Assumptions on Demand
Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. Proceedings of the 30th international conference of computer aided verifacation. CAV: Computer Aided Verification, Lecture Notes in Computer Science, vol. 5123, 314–327.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Author
Podelski, Andreas;
Rybalchenko, Andrey;
Wies, ThomasISTA
Series Title
Lecture Notes in Computer Science
Abstract
Termination of a heap-manipulating program generally depends on preconditions that express heap assumptions (i.e., assertions describing reachability, aliasing, separation and sharing in the heap). We present an algorithm for the inference of such preconditions. The algorithm exploits a unique interplay between counterexample-producing abstract termination checker and shape analysis. The shape analysis produces heap assumptions on demand to eliminate counterexamples, i.e., non-terminating abstract computations. The experiments with our prototype implementation indicate its practical potential.
Publishing Year
Date Published
2008-07-07
Proceedings Title
Proceedings of the 30th international conference of computer aided verifacation
Publisher
Springer Nature
Volume
5123
Page
314 - 327
Conference
CAV: Computer Aided Verification
Conference Location
Princeton, NJ, United Stated
Conference Date
2008-07-07 – 2008-07-14
ISBN
IST-REx-ID
Cite this
Podelski A, Rybalchenko A, Wies T. Heap Assumptions on Demand. In: Proceedings of the 30th International Conference of Computer Aided Verifacation. Vol 5123. Springer Nature; 2008:314-327. doi:10.1007/978-3-540-70545-1_31
Podelski, A., Rybalchenko, A., & Wies, T. (2008). Heap Assumptions on Demand. In Proceedings of the 30th international conference of computer aided verifacation (Vol. 5123, pp. 314–327). Princeton, NJ, United Stated: Springer Nature. https://doi.org/10.1007/978-3-540-70545-1_31
Podelski, Andreas, Andrey Rybalchenko, and Thomas Wies. “Heap Assumptions on Demand.” In Proceedings of the 30th International Conference of Computer Aided Verifacation, 5123:314–27. Springer Nature, 2008. https://doi.org/10.1007/978-3-540-70545-1_31.
A. Podelski, A. Rybalchenko, and T. Wies, “Heap Assumptions on Demand,” in Proceedings of the 30th international conference of computer aided verifacation, Princeton, NJ, United Stated, 2008, vol. 5123, pp. 314–327.
Podelski A, Rybalchenko A, Wies T. 2008. Heap Assumptions on Demand. Proceedings of the 30th international conference of computer aided verifacation. CAV: Computer Aided Verification, Lecture Notes in Computer Science, vol. 5123, 314–327.
Podelski, Andreas, et al. “Heap Assumptions on Demand.” Proceedings of the 30th International Conference of Computer Aided Verifacation, vol. 5123, Springer Nature, 2008, pp. 314–27, doi:10.1007/978-3-540-70545-1_31.
Google Scholar
ISBN Search