Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Verification of heap manipulating programs with ordered data by extended forest automata

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Notes

  1. The use of \(\ne \) is forbidden because it would lead to a disjunction of constraints, which we do not support in this work.

  2. Note that from the definitions of languages of TAs and FAs, the effect of the \(\sim _{\mathtt {ra}}\) data constraint (both local and global) is local to the TAs it is related to.

References

  1. Abdulla, P.A., Atto, M., Cederberg, J., Ji, R.: Automated analysis of data-dependent programs with dynamic memory. In Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis–ATVA’09, volume 5799 of LNCS, pp. 197–212. Springer, Berlin (2009)

  2. Abdulla, P.A., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems–TACAS’13, volume 7795 of LNCS, pp. 324–338. Springer (2013)

  3. Abdulla, P., Holík, L., Jonsson, B., Lengál, O., Trinh, C. Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. In Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis–ATVA’13, volume 8172 of LNCS, pp. 224–239. Springer (2013)

  4. Beyer, D., Henzinger, T.A., Théoduloz, G.: Lazy shape analysis. In Proceedings of the 18th International Conference on Computer Aided Verification–CAV’06, volume 4144 of LNCS, pp. 532–546. Springer (2006)

  5. Bingham, J., Rakamarić, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation–VMCAI’06, volume 3855 of LNCS, pp. 207–221. Springer (2006)

  6. Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Form. Methods Syst. Des. 38(2), 158–192 (2011)

    Article  MATH  Google Scholar 

  7. Bouajjani, A., Drăgoi, C., Enea, C., Sighireanu, M.: Accurate invariant checking for programs manipulating lists and arrays with infinite data. In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis–ATVA’12, volume 7561 of LNCS, pp 167–182. Springer (2012)

  8. Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 167–191 (2012)

    Article  MATH  Google Scholar 

  9. Chang, B.-Y. E., Rival, X.: Relational inductive shape analysis. In Proceedings of the 35th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages–POPL’08, pp. 247–260. ACM (2008)

  10. Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In Proceedings of the 14th International Static Analysis Symposium–SAS’07, volume 4634 of LNCS, pp. 384–401. Springer (2007)

  11. Chatterjee, S., Lahiri, S. K., Qadeer, S., Rakaramarić, Z.: A reachability predicate for analyzing low-level software. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems–TACAS’07, volume 4424 of LNCS, pp. 19–33. Springer (2007)

  12. Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006–1036 (2012)

    Article  MATH  Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages–POPL’77, pp. 238–252. ACM (1977)

  14. Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In Proceedings of the 20th International Static Analysis Symposium–SAS’13, volume 7935 of LNCS, pp. 215–237. Springer (2013)

  15. Habermehl, P., Holík, L., Rogalewicz, A., Šimáček, J., Vojnar, T.: Forest automata for verification of heap manipulation. Form. Methods Syst. Des. 41(1), 83–106 (2012)

    Article  MATH  Google Scholar 

  16. Heinen, J., Noll, T., Rieger, S.: Juggrnaut: Graph grammar abstraction for unbounded heap structures. In Proceedings of the 3rd International Workshop on Harnessing Theories for Tool Support in Software–TTSS’09, volume 266 of ENTCS, pp. 93–107. Elsevier (2010)

  17. Holík, L., Lengál, O., Rogalewicz, A., Šimáček, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In Proceedings of the 25th International Conference on Computer Aided Verification–CAV’13, volume 8044 of LNCS, pp. 740–755. Springer (2013)

  18. Jensen, J.L., Jørgensen, M. E., Schwartzbach, M. I., Klarlund, N.: Automatic verification of pointer programs using monadic second-order logic. In Proceedings of the 1997 ACM SIGPLAN Conference on Programming Language Design and Implementation–PLDI’97, pp. 226–234. ACM (1997)

  19. Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In Proceedings of the 35th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages–POPL’08, pp. 171–182. ACM (2008)

  20. Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In Proceedings of the 17th International Conference on Computer Aided Verification–CAV’05, volume 3576 of LNCS, pp. 519–533. Springer (2005)

  21. Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In Proceedings of the 37th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages–POPL’10, pp. 211–222. ACM (2010)

  22. McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In Proceedings of the 17th International Conference on Computer Aided Verification–CAV’05, volume 3576 of LNCS, pp. 476–490. Springer (2005)

  23. Pugh, W.: Skip lists: a probabilistic alternative to balanced trees. Commun ACM 33(6), 668–676 (1990)

    Article  MathSciNet  Google Scholar 

  24. Qin, S., He, G., Luo, C., Chin, W.-N., Chen, X.: Loop invariant synthesis in a combined abstract domain. J. Symb. Comput. 50, 386–408 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  25. Rakamarić, Z., Bruttomesso, R., Hu, A.J., Cimatti, A.: Verifying heap-manipulating programs in an SMT framework. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis–ATVA’07, volume 4762 of LNCS, pp. 237–252. Springer (2007)

  26. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

    Article  Google Scholar 

  27. Wies, T., Kuncak, V., Zee, K., Podelski, A., Rinard, M.: On verifying complex properties using symbolic shape analysis. In Proceedings of Heap Analysis and Verification 2007–HAV’07 (2007)

  28. Wies, T., Podelski, A.: Counterexample-guided focus. In Proceedings of the 37th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages–POPL’10, pp. 249–260. ACM (2010)

  29. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In Proceedings of the 20th International Conference on Computer Aided Verification–CAV’08, volume 5123 of LNCS, pp. 385–398. Springer (2008)

  30. Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation–PLDI’08, pp. 349–361. ACM (2008)

Download references

Acknowledgments

We thank the anonymous reviewers for their useful feedback on the paper.

Author information

Authors and Affiliations

  1. Department of Information Technology, Uppsala University, Box 337, 751 05, Uppsala, Sweden

    Parosh Aziz Abdulla, Bengt Jonsson & Cong Quy Trinh

  2. FIT, IT4Innovations Centre of Excellence, Brno University of Technology, Božetěchova 2, 61266, Brno, Czech Republic

    Lukáš Holík, Ondřej Lengál & Tomáš Vojnar

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lukáš Holík
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ondřej Lengál
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Cong Quy Trinh
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Tomáš Vojnar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ondřej Lengál.

Additional information

This paper is an extended version of a paper published in the proceedings of ATVA’13. The work was supported by the Czech Science Foundation (Projects 14-11384S and 13-37876P), the internal BUT project FIT-S-14-2486, the EU/Czech IT4Innovations Centre of Excellence Project CZ.1.05/1.1.00/02.0070, the Swedish Foundation for Strategic Research within the ProFuN project, and by the Swedish Research Council within the UPMARC centre of excellence.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Abdulla, P.A., Holík, L., Jonsson, B. et al. Verification of heap manipulating programs with ordered data by extended forest automata. Acta Informatica 53, 357–385 (2016). https://doi.org/10.1007/s00236-015-0235-0

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-015-0235-0

Search

Navigation