Abstract
If program verification tools are ever to be used widely, it is essential that they work in a modular fashion. Otherwise, verification will not scale. This paper discusses the scientific challenges that this poses for research in program logic. Some recent work on separation logic is described, and test problems that would be useful in measuring advances on modular reasoning are suggested.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Amadi, M., Lamport, L.: Composing specifications. ACM TOPLAS 15(1), 73–132 (1993)
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)
Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. J.ACM (to appear, 2005)
Barnett, M., DeLine, R., Fahndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Automatic modular assertion checking with separation logic. In: 4th FMCO, pp. 115–137 (2006)
Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.W.: Variance analyses from invariance analyses. In: 34th POPL, pp. 211–224 (2007)
Berdine, J., 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)
Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM TOPLAS (to appear, 2007)
Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Transactions of Software Engineering 21, 809–838 (1995)
Bornat, R., Calcagno, C., Yang, H.: Variables as resources in separation logic. In: 19th MFPS (2005)
Brookes, S.D.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 227–270. Springer, Heidelberg (2004)
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 182–203. Springer, Heidelberg (2006)
Clarke, D., Noble, J., Potter, J.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 53–76. Springer, Heidelberg (2001)
Cok, D., Kiniry, J.: ESC/Java2: Uniting ESC/Java and JML. In: CASSIS, pp. 108–128 (2004)
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: 13th PLDI (2006)
Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT) (to appear, 2005)
Distefano, D., O’Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: 12th TACAS, pp. 287–302 (2006)
Feng, X., Ferreira, R., Shao, Z.: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173–188. Springer, Heidelberg (2007)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: 9th PLDI (2002)
Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI (to appear, 2007)
Guo, B., Vachharajani, N., August, D.: Shape analysis with inductive recursion synthesis. In: PLDI (to appear, 2007)
Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engler, E. (ed.) Symposium on the Semantics of Algebraic Languages. Lecture Notes in Math. vol. 188, pp. 102–116. Springer, Heidelberg (1971)
Hoare, C.A.R.: Towards a theory of parallel programming. In: Hoare, Perrot (eds.) Operating Systems Techniques, Academic Press, London (1972)
Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. J. ACM 50(1), 63–69 (2003)
Hogg, J.: Islands: aliasing protection in object-oriented languages. In: 6th OOPSLA (1991)
Isthiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, January 2001, pp. 36–49 (2001)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Conference (1983)
Jones, C.B.: Wanted: A compositional approach to concurrency. In: McIver, A., Morgan, C. (eds.) Programming Methodology, pp. 1–15. Springer, Heidelberg (2003)
Leavens, G.T., Leino, K.R.M., Müller, P.: Specification and verification challenges for sequential object-oriented programs. In: Formal Aspects of Computing (to appear, 2007)
Leino, K.R.M., Müller, P.: Object Invariants in Dynamic Contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491–515. Springer, Heidelberg (2004)
Leino, K.R.M., Müller, P.: A Verification Methodology for Model Fields. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 115–130. Springer, Heidelberg (2006)
Marti, N., Affeldt, R., Yonezawa, A.: Verification of the heap manager of an operating system using separation logic. In: Proceedings of the 3rd SPACE Workshop, Charleston (2006)
McCarthy, J., Hayes, P.: Some philosophical problems from the standpoint of artificial intelligence. In: Machine Intelligence, vol. 4, pp. 463–502 (1969)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential types. ACM Trans. Programming Languages and Systems 10(3), 470–502 (1988)
Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. In: 19th LICS, pp. 313–323 (2004)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of 15th Annual Conference of the European Association for Computer Science Logic. LNCS, pp. 1–19. Springer, Heidelberg (2001)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: 31st POPL, pp. 268–280 (2004)
O’Hearn, P.W.: Resources, Concurrency and Local Reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49–67. Springer, Heidelberg (2004)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proceedings of POPL (2005)
Parkinson, M., Vafeiadis, V.: A Marriage of Rely/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)
Podelski, A., Rybalchenko, A.: Transition invariants. In: 19th LICS (2004)
Rabinovich, A.: On compositionality and its limitations. ACM TOCL 8(1), 73–132 (2007)
Reiter, R.: The frame problem in the situation calculus: a simple solution (sometimes) and a completeness result for goal regression. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 359–380. Academic Press, London (1991)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Proceedings of IFIP (1983)
Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Houndsmill, Hampshire, Palgrave, pp. 303–321 (2000)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th LICS, pp. 55–74 (2002)
Stark, E.W.: A proof technique for rely/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol. 206, pp. 369–391. Springer, Heidelberg (1985)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: 34th POPL (2007)
Yang, H.: Local Reasoning for Stateful Programs. Ph.D. thesis, University of Illinois, Urbana-Champaign (2001)
Yang, H., O’Hearn, P.W.: A Semantic Basis for Local Reasoning. In: Nielsen, M., Engberg, U. (eds.) ETAPS 2002 and FOSSACS 2002. LNCS, vol. 2303, Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
O’Hearn, P.W. (2008). Scalable Specification and Reasoning: Challenges for Program Logic. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)