Article

Heap Assumptions on Demand

Authors:

Andreas Podelski,

Andrey Rybalchenko,

Thomas WiesAuthors Info & Claims

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

Pages 314 - 327

https://doi.org/10.1007/978-3-540-70545-1_31

Published: 07 July 2008 Publication History

Abstract

Termination of a heap-manipulating program generally depends on preconditions that express <em>heap assumptions</em>(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.

References

[1]

Berdine, J., Calcagno, C., Cook, B., Distefano, D., O'Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178-192. Springer, Heidelberg (2007)

Digital Library

[2]

Berdine, J., Cook, B., Distefano, D., O'Hearn, P.: Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386-400. Springer, Heidelberg (2006)

Digital Library

[3]

Beyer, D., Henzinger, T.A., Théoduloz, G.: Lazy shape analysis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 532-546. Springer, Heidelberg (2006)

Digital Library

[4]

Bogudlov, I., Lev-Ami, T., Reps, T.W., Sagiv, M.: Revamping TVLA: Making parametric shape analysis competitive. In: Damm,W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 221-225. Springer, Heidelberg (2007)

Digital Library

[5]

Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 517- 531. Springer, Heidelberg (2006)

Digital Library

[6]

Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking of complex dynamic data structures. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 52-70. Springer, Heidelberg (2006)

Digital Library

[7]

Bradley, A., Manna, Z., Sipma, H.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1349- 1361. Springer, Heidelberg (2005)

Digital Library

[8]

Calcagno, C., Distefano, D., O'Hearn, P., Yang, H.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402-418. Springer, Heidelberg (2007)

Digital Library

[9]

Colón, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404. Springer, Heidelberg (2002)

Digital Library

[10]

Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI (2006)

Digital Library

[11]

Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1-24. Springer, Heidelberg (2005)

Digital Library

[12]

Distefano, D., O'Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 287- 302. Springer, Heidelberg (2006)

Digital Library

[13]

Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL (2005)

Digital Library

[14]

Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)

Digital Library

[15]

Magill, S., Berdine, J., Clarke, E.M., Cook, B.: Arithmetic strengthening for shape analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 419-436. Springer, Heidelberg (2007)

Digital Library

[16]

Manolios, P., Vroon, D.: Termination Analysis with Calling Context Graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 401-414. Springer, Heidelberg (2006)

Digital Library

[17]

Maus, S.: Developing an Operating System Kernel for the VAMP Processor. Diploma thesis, Universität des Saarlandes (2005)

[18]

Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245- 259. Springer, Heidelberg (2006)

Digital Library

[19]

Podelski, A., Rybalchenko, A., Wies, T.: Heap assumptions on demand. Technical report, University of Freiburg (2008), http://www.informatik.uni-freiburg.de/ wies/papers/. HeapAssumptionsExtended.pdf.

[20]

Podelski, A., Wies, T.: Boolean Heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 268-283. Springer, Heidelberg (2005)

Digital Library

[21]

Rybalchenko, A.: ARMC (2008), http://www.mpi-sws.org/~rybal/armc

[22]

Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS (2002)

Digital Library

[23]

Wies, T.: Symbolic Shape Analysis. Diploma thesis, Universität des Saarlandes, Germany (2004)

[24]

Wies, T.: The Bohne Tool (2008), http://swt.informatik.uni-freiburg.de/wies/bohne

[25]

Wies, T., Kuncak, V., Zee, K., Podelski, A., Rinard, M.: Verifying complex properties using symbolic shape analysis. In: HAV Workshop (2007)

Cited By

Kleine Büning MMeuer JSinz C(2022)Refined Modularization for Bounded Model Checking Through Precondition GenerationFormal Methods and Software Engineering10.1007/978-3-031-17244-1_13(209-226)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-17244-1_13
Chen YHeizmann MLengál OLi YTsai MTurrini AZhang L(2018)Advanced automata-based algorithms for program termination checkingACM SIGPLAN Notices10.1145/3296979.319240553:4(135-150)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192405
Chen YHeizmann MLengál OLi YTsai MTurrini AZhang LFoster JGrossman D(2018)Advanced automata-based algorithms for program termination checkingProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192405(135-150)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192405
Show More Cited By

Recommendations

Learning Assumptions for CompositionalVerification of Timed Systems

Compositional techniques such as assume-guarantee reasoning (AGR) can help to alleviate the state space explosion problem associated with model checking. However, compositional verification is difficult to be automated, especially for timed systems, ...
Symbolic heap abstraction with demand-driven axiomatization of memory invariants
OOPSLA '10: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

Many relational static analysis techniques for precise reasoning about heap contents perform an explicit case analysis of all possible heaps that can arise. We argue that such precise relational reasoning can be obtained in a more scalable and ...
Model checking recursive programs interacting via the heap

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive procedures and local ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

July 2008

555 pages

ISBN:9783540705437

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 July 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kleine Büning MMeuer JSinz C(2022)Refined Modularization for Bounded Model Checking Through Precondition GenerationFormal Methods and Software Engineering10.1007/978-3-031-17244-1_13(209-226)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-17244-1_13
Chen YHeizmann MLengál OLi YTsai MTurrini AZhang L(2018)Advanced automata-based algorithms for program termination checkingACM SIGPLAN Notices10.1145/3296979.319240553:4(135-150)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192405
Chen YHeizmann MLengál OLi YTsai MTurrini AZhang LFoster JGrossman D(2018)Advanced automata-based algorithms for program termination checkingProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192405(135-150)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192405
Margoor AKomondoor R(2015)Two techniques to improve the precision of a demand-driven null-dereference verification approachScience of Computer Programming10.1016/j.scico.2014.09.00698:P4(645-679)Online publication date: 1-Feb-2015
https://dl.acm.org/doi/10.1016/j.scico.2014.09.006
Ganty PGenaim S(2013)Proving Termination Starting from the EndProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958105(397-412)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958105
Bansal KKoskinen EWies TZufferey D(2013)Structural counter abstractionProceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-36742-7_5(62-77)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-36742-7_5
Cousot PCousot RFähndrich MLogozzo F(2013)Automatic Inference of Necessary PreconditionsProceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 773710.1007/978-3-642-35873-9_10(128-148)Online publication date: 20-Jan-2013
https://dl.acm.org/doi/10.1007/978-3-642-35873-9_10
Brockschmidt MMusiol ROtto CGiesl J(2012)Automated termination proofs for Java programs with cyclic dataProceedings of the 24th international conference on Computer Aided Verification10.1007/978-3-642-31424-7_13(105-122)Online publication date: 7-Jul-2012
https://dl.acm.org/doi/10.1007/978-3-642-31424-7_13
Calcagno CDistefano DO’Hearn PYang H(2011)Compositional Shape Analysis by Means of Bi-AbductionJournal of the ACM10.1145/2049697.204970058:6(1-66)Online publication date: 1-Dec-2011
https://dl.acm.org/doi/10.1145/2049697.2049700
Gulavani BChakraborty SRamalingam GNori A(2011)Bottom-up shape analysis using LISFACM Transactions on Programming Languages and Systems10.1145/2039346.203934933:5(1-41)Online publication date: 23-Nov-2011
https://dl.acm.org/doi/10.1145/2039346.2039349
Show More Cited By

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents