Skip to main content
SpringerLink
Log in

A Machine-Checked Framework for Relational Separation Logic

  • Conference paper
Software Engineering and Formal Methods (SEFM 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7041))

Included in the following conference series:

  • 923 Accesses

Abstract

Relational methods are gaining growing acceptance for specifying and verifying properties defined in terms of the execution of two programs—notions such as simulation, observational equivalence, non-interference, and continuity can be elegantly cast in this setting. In previous work, we have proposed program product construction as a technique to reduce relational verification to standard verification. This method hinges on the ability to interpret relational assertions as traditional predicates, which becomes problematic when considering assertions from relational separation logic. We report in this article an alternative method that overcomes this difficulty, defined as a relational weakest precondition calculus based on separation logic and formalized in the Coq proof assistant. The formalization includes an application to the formal verification of the Schorr-Waite graph marking algorithm. We discuss additional variants of relational separation logic inspired by the standard notions of partial and total correctness, and extensions of the logic to handle non-structurally equivalent programs.

Partially funded by European Projects FP7-231620 HATS and FP7-256980 NESSoS, Spanish project TIN2009-14599 DESAFIOS 10, Madrid Regional project S2009TIC-1465 PROMETIDOS. César Kunz is funded by a Juan de la Cierva Fellowship, MICINN, Spain.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Morrisett, G., Peyton Jones, S. (eds.) Principles of Programming Languages, pp. 91–102. ACM, New York (2006)

    Google Scholar 

  2. Appel, A.: Tactics for separation logic (January 2006) (unpublished manuscript), http://www.cs.princeton.edu/~appel/papers/septacs.pdf

  3. Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: Shao, Z., Pierce, B.C. (eds.) Principles of Programming Languages, pp. 90–101. ACM Press, New York (2009)

    Google Scholar 

  6. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  7. Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Principles of Programming Languages, pp. 14–25. ACM Press, New York (2004)

    Google Scholar 

  8. Beringer, L.: Relational program logics in decomposed style (2010) (submitted)

    Google Scholar 

  9. Bodík, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: Principles of Programming Languages, pp. 339–352 (2010)

    Google Scholar 

  10. Bornat, R.: Proving pointer programs in hoare logic. In: Backhouse, R.C., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Gast, H.: Lightweight separation. In: Mohamed, O., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 199–214. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Giorgino, M., Strecker, M., Matthes, R., Pantel, M.: Verification of the Schorr-Waite algorithm - From trees to graphs (January 2010)

    Google Scholar 

  13. Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don’t block. In: Shao, Z., Pierce, B.C. (eds.) Principles of Programming Languages, pp. 16–28. ACM, New York (2009)

    Google Scholar 

  14. Hubert, T., Marché, C.: A case study of c source code verification: the schorr-waite algorithm. In: Aichernig, B., Beckert, B. (eds.) Software Engineering and Formal Methods, pp. 190–199. IEEE Computer Society, Los Alamitos (2005)

    Google Scholar 

  15. Ishtiaq, S., O’Hearn, P.: BI as an assertion language for mutable data structures. In: Principles of Programming Languages, pp. 14–26 (2001)

    Google Scholar 

  16. Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Katholieke Universiteit Leuven (2008)

    Google Scholar 

  17. Jacobs, B., Smans, J., Piessens, F.: Verifying the composite pattern using separation logic. In: Workshop on Specification and Verification of Component-Based Systems, Challenge Problem Track (November 2008)

    Google Scholar 

  18. McCreight, A.: Practical tactics for separation logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 343–358. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Inf. Comput. 199(1-2), 200–227 (2005)

    Article  MATH  Google Scholar 

  20. Myreen, M.O.: Separation logic adapted for proofs by rewriting. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 485–489. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: Hermenegildo, M., Palsberg, J. (eds.) Principles of Programming Languages, pp. 261–274. ACM, New York (2010)

    Google Scholar 

  22. Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: 2011 IEEE Symposium on Security and Privacy. IEEE Computer Society, Los Alamitos (2011)

    Google Scholar 

  23. O’Hearn, P.W., Reynolds, J., 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)

    Chapter  Google Scholar 

  24. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)

    Google Scholar 

  25. Suzuki, N.: Automatic Verification of Programs with Complex Data Structures. PhD thesis, Stanford University (1976)

    Google Scholar 

  26. Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Principles of Programming Languages, pp. 97–108. ACM, New York (2007)

    Google Scholar 

  27. Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  28. Yang, H.: Local reasoning for stateful programs. PhD thesis, University of Illinois, Urbana, IL, USA (2001)

    Google Scholar 

  29. Yang, H.: Relational separation logic. Theoretical Computer Science 375(1-3), 308–334 (2007)

    Article  MATH  Google Scholar 

  30. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Madrid, Spain

    Juan Manuel Crespo & César Kunz

  2. Universidad Politécnica de Madrid, Spain

    César Kunz

Authors
  1. Juan Manuel Crespo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. César Kunz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fundación IMDEA Software, Facultad de Informatica (UPM), Campus Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Gilles Barthe

  2. Instituto de Computación, Universidad de la República, Facultad de Ingeniería, Julio Herrera y Reissig 565 - Piso 5, 11300, Montevideo, Uruguay

    Alberto Pardo

  3. Department of Computer Science and Engineering, Chalmers | University of Gothenburg, Kunskapsgatan 3, 41756, Gothenburg, Sweden

    Gerardo Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Crespo, J.M., Kunz, C. (2011). A Machine-Checked Framework for Relational Separation Logic. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24690-6_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-24689-0

  • Online ISBN: 978-3-642-24690-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation