Abstract
An algebraic approach to the design of program construction and verification tools is applied to separation logic. The control-flow level is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data domain is captured by concrete store-heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation or refinement laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof assistant simple and highly automatic. The resulting tool is itself correct by construction; it is explained on three simple examples.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Armstrong, A., Gomes, V.B.F., Struth, G.: Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 78–93. Springer, Heidelberg (2014)
Armstrong, A., Gomes, V.B.F., Struth, G.: Lightweight program construction and verification tools in Isabelle/HOL. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 5–19. Springer, Heidelberg (2014)
Back, R.-J., von Wright, J.: Refinement Calculus. Springer, Berlin (1999)
Bergelson, V., Blass, A., Hindman, N.: Partition theorems for spaces of variable words. Proc. London Math. Soc. 68(3), 449–476 (1994)
Berstel, J., Reutenauer, C.: Les séries rationnelles et leurs langagues. Masson (1984)
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 259–270. ACM (2005)
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007, pp. 366–378. IEEE Computer Society (2007)
Chlipala, A., Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: Hutton, G., Tolmach, A.P. (eds.) ICFP 2009, pp. 79–90. ACM (2009)
Dang, H.-H., Höfner, P., Möller, B.: Algebraic separation logic. J. Log. Algebr. Program. 80(6), 221–247 (2011)
Dang, H.-H., Möller, B.: Transitive separation logic. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 1–16. Springer, Heidelberg (2012)
Dang, H.-H., Möller, B.: Concurrency and local reasoning under reverse interchange. Sci. Comput. Program. 85, 204–223 (2014)
Day, B.: On closed categories of functors. In: MacLane, S., et al. (eds.) Reports of the Midwest Category Seminar IV. Lecture Notes in Mathematics, vol. 137, pp. 1–38. Springer, Heidelberg (1970)
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: Giacobazzi, R., Cousot, R. (eds.) POPL, pp. 287–300. ACM (2013)
Distefano, D., Parkinson, M.J.: jstar: towards practical verification for Java. In: Harris, G.E. (ed.) OOPSLA 2008, pp. 213–226. ACM (2008)
Dongol, B., Hayes, I.J., Struth, G.: Convolution, separation and concurrency. CoRR, abs/1312.1225 (2014)
Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata, 1st edn. Springer, Heidelberg (2009)
Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 215–237. Springer, Heidelberg (2013)
Gardiner, P.H.B., Martin, C.E., de Moor, O.: An algebraic construction of predicate transformers. Sci. Comput. Program. 22(1–2), 21–44 (1994)
Guttmann, W., Struth, G., Weber, T.: Automating algebraic methods in Isabelle. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 617–632. Springer, Heidelberg (2011)
Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G.: On locality and the exchange law for concurrent processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 250–264. Springer, Heidelberg (2011)
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM TOPLAS 5(4), 596–619 (1983)
Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332–337. Springer, Heidelberg (2012)
Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM TOCL 1(1), 60–76 (2000)
Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1–2), 200–227 (2005)
Möller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoret. Comput. Sci. 351(2), 221–239 (2006)
Morgan, C.: Programming from Specifications. Prentice-Hall, New York (1998)
Naumann, D.A.: Beyond fun: order and membership in polytypic imperative programming. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 286–314. Springer, Heidelberg (1998)
Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theoret. Comput. Sci. 375(1–3), 271–307 (2007)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symbolic Logic 5(2), 215–244 (1999)
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319–340 (1976)
Preoteasa, V.: Algebra of monotonic boolean transformers. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 140–155. Springer, Heidelberg (2011)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)
Smans, J., Jacobs, B., Piessens, F.: VeriFast for Java: a tutorial. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol. 7850, pp. 407–442. Springer, Heidelberg (2013)
Tuerk, T.: A Separation Logic Framework for HOL. Ph.D. thesis, Computer Laboratory, University of Cambridge (2011)
V. Vafeiadis. Modular Fine-Grained Concurrency Verificaiton. PhD thesis, Computer Laboratory, University of Cambridge, 2007
van Staden, S.: Constructing the Views Framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 62–83. Springer, Heidelberg (2015)
Weber, T.: Towards Mechanized Program Verification with Separation Logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 250–264. Springer, Heidelberg (2004)
Yang, H., O’Hearn, P.W.: A Semantic Basis for Local Reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)
Acknowledgements
We are grateful for support by EPSRC grant EP/J003727/1 and the CNPq. The third author would like to thank Tony Hoare, Peter O’Hearn and Matthew Parkinson for discussions on concurrent Kleene algebra and separation logic.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Dongol, B., Gomes, V.B.F., Struth, G. (2015). A Program Construction and Verification Tool for Separation Logic. In: Hinze, R., Voigtländer, J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science(), vol 9129. Springer, Cham. https://doi.org/10.1007/978-3-319-19797-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-19797-5_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19796-8
Online ISBN: 978-3-319-19797-5
eBook Packages: Computer ScienceComputer Science (R0)