Abstract
Automatically verifying heap-manipulating programs is a challenging task, especially when dealing with complex data structures with strong invariants, such as sorted lists and AVL/red-black trees. The verification process can greatly benefit from human assistance through specification annotations, but this process requires intellectual effort from users and is error-prone. In this paper, we propose a new approach to program verification that allows users to provide only partial specification to methods. Our approach will then refine the given annotation into a more complete specification by discovering missing constraints. The discovered constraints may involve both numerical and multi-set properties that could be later confirmed or revised by users. We further augment our approach by requiring only partial specification to be given for primary methods. Specifications for loops and auxiliary methods can then be systematically discovered by our augmented mechanism, with the help of information propagated from the primary methods. Our work is aimed at verifying beyond shape properties, with the eventual goal of analysing full functional properties for pointer-based data structures. Initial experiments have confirmed that we can automatically refine partial specifications with non-trivial constraints, thus making it easier for users to handle specifications with richer properties.
This work is supported in part by EPSRC project EP/G042322 and MoE ARF grant R-252-000-411-112.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Barry, R.: FreeRTOS — a free RTOS for small embedded real time systems (2006)
Bouajjani, A., Dragoi, C., Enea, C., Rezine, A., Sighireanu, M.: Invariant synthesis for programs manipulating lists with unbounded data. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 72–88. Springer, Heidelberg (2010)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K.: An Overview of JML Tools and Applications. STTT 7(3), 212–232 (2005)
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009)
Chang, B., Rival, X.: Relational inductive shape analysis. In: POPL (2008)
Chatterjee, S., Lahiri, S., Qadeer, S., Rakamaric, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)
Cousot, P., Cousot, R.: On abstraction in software verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 37. Springer, Heidelberg (2002)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)
Giacobazzi, R.: Abductive analysis of modular logic programs. In: ILPS (1994)
Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240–260. Springer, Heidelberg (2006)
Gulavani, B., Chakraborty, S., Ramalingam, G., Nori, A.: Bottom-up shape analysis. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 188–204. Springer, Heidelberg (2009)
Gulwani, S., Lev-Ami, T., Sagiv, M.: A Combination Framework for Tracking Partition Sizes. In: POPL (2009)
Gupta, A., Majumdar, R., Rybalchenko, A.: From tests to proofs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 262–276. Springer, Heidelberg (2009)
Gustavsson, J., Svenningsson, J.: Constraint abstractions. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, p. 63. Springer, Heidelberg (2001)
Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: POPL (2005)
Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: PLDI (2009)
Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)
Magill, S., Berdine, J., Clarke, E., 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)
Magill, S., Tsai, M., Lee, P., Tsay, Y.: THOR: A tool for reasoning about shape and arithmetic. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 428–432. Springer, Heidelberg (2008)
Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: POPL (2010)
Møller, A., Schwartzbach, M.: The pointer assertion logic engine. ACM SIGPLAN Notices 36(5), 221–231 (2001)
Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — a proof assistant for higher-order logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2008)
Qin, S., He, G., Luo, C., Chin, W.-N.: Loop invariant synthesis in a combined domain. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 468–484. Springer, Heidelberg (2010)
Qin, S., Luo, C., Chin, W.-N., He, G.: Automatically Refining Partial Specification for Program Verification. Technical Report, Teesside University (2010), http://www.scm.tees.ac.uk/s.qin/papers/refine.pdf
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS 2002 (2002)
Rondon, P., Kawaguci, M., Jhala, R.: Liquid types. In: PLDI (2008)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)
Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI (2009)
Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Qin, S., Luo, C., Chin, WN., He, G. (2011). Automatically Refining Partial Specifications for Program Verification. In: Butler, M., Schulte, W. (eds) FM 2011: Formal Methods. FM 2011. Lecture Notes in Computer Science, vol 6664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21437-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-21437-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21436-3
Online ISBN: 978-3-642-21437-0
eBook Packages: Computer ScienceComputer Science (R0)