Abstract
Separation logic is a key development in formal reasoning about programs, opening up new lines of attack on longstanding problems.
Supplemental Material
Available for Download
Supplemental material.
- Appel, A.W. Program Logics for Certified Compilers. Cambridge University Press, U.K., 2014. Google ScholarCross Ref
- Berdine, J. Calcagno, C. and O'Hearn, P.W. Smallfoot: Modular automatic assertion checking with separation logic. LNCS FMCO 4111 (2005) 115--137, 2005. Google ScholarDigital Library
- Berdine, J., Cook, B. and Ishtiaq, S. SLAyer: Memory safety for systems-level code. In Proceedings of CAV, 2011, 178--183. Google ScholarDigital Library
- Beringer, L., Petcher, A., Ye, K.Q. and Appel, A.W. Verified correctness and security of OpenSSL HMAC. In Proceedings of 24<sup>th</sup> USENIX Security Symposium, 2015, 207--221. Google ScholarDigital Library
- Biering, B., Birkedal, L. and Torp-Smith, N. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM TOPLAS 29, 4 (2007). Google ScholarDigital Library
- Bornat, R. Proving pointer programs in Hoare logic. LNCS MPC 1837 (2000) 102--126. Google ScholarDigital Library
- Bornat, R., Calcagno, C., O'Hearn, P.W. and Parkinson, M.J. Permission accounting in separation logic. In Proceedings of POPL, 2005, 259--270. Google ScholarDigital Library
- Brookes, S. A semantics for concurrent separation logic. Theor. Comput. Sci., 375, 1--3 (2007), 227--270. Google ScholarDigital Library
- Brookes, S. and O'Hearn, P.W. Concurrent separation logic. SIGLOG News 3, 3 (2016), 47--65. Google ScholarDigital Library
- Burstall, R.M. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 1 (1972), 23--50.Google Scholar
- Calcagno, C. et al. Moving fast with software verification. In Proceedings of NASA Formal Methods Symposium, 2015, 3--11.Google ScholarCross Ref
- Calcagno, C., Distefano, D., O'Hearn, P.W. and Yang, H. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6 (2011), 26. Preliminary version in Proceedings of POPL'09. Google ScholarDigital Library
- Calcagno, C., O'Hearn, P.W. and Yang, H. Local action and abstract separation logic. LICS, 2007, 366--378. Google ScholarDigital Library
- Chen, H., Ziegler, F., Chajed, T., Chlipala, A., Kaashoek, M.F. and Zeldovich, N. Using Crash Hoare logic for certifying the FSCQ file system. In Proceedings of SOSP, pages 18--37, 2015. Google ScholarDigital Library
- Cousot, P. and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL, 1977, 238--252. Google ScholarDigital Library
- Dijkstra, E.W. Cooperating sequential processes. Programming Languages, Academic Press, 1968, 43--112.Google Scholar
- Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J. and Yang, H. Views: Compositional reasoning for concurrent programs. In Proceedings of POPL, 2013, 287--300. Google ScholarDigital Library
- Dinsdale-Young, T., Dodds, M., Gardner, M., Parkinson, M.J. and Vafeiadis, V. Concurrent abstract predicates. In Proceedings of ECOOP, 2010, 504--528. Google ScholarDigital Library
- Dinsdale-Young, T., Gardner, P. and Wheelhouse, M.J. Abstraction and refinement for local reasoning. In Proceedings of VSTTE, 2010, 199--215. Google ScholarDigital Library
- Distefano, D., O'Hearn, P.W. and Yang, H. A local shape analysis based on separation logic. In Proceedings of TACAS, 2006, 287--302. Google ScholarDigital Library
- Floyd, R.W. Assigning meanings to programs. In Proceedings of the Symposium on Applied Mathematics. J.T. Schwartz, ed. AMS, 1967, 19--32.Google ScholarCross Ref
- Hoare, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576--580. Google ScholarDigital Library
- Hoare, C.A.R. Towards a theory of parallel programming. Operating Systems Techniques. Academic Press, 1972.Google Scholar
- Hoare, T., Möller, B., Struth, G. and Wehrman, I. Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program 80, 6 (2011), 266--296.Google ScholarCross Ref
- Hobor, A. and Villard, J. The ramifications of sharing in data structures. In Proceedings of 40<sup>th</sup> POPL, 2013, 523--536. Google ScholarDigital Library
- Ishtiaq, S.S. and O'Hearn, P.W. BI as an assertion language for mutable data structures. In Proceedings of POPL, 2001, 14--26. Google ScholarDigital Library
- Jones, C.B. Specification and design of (parallel) programs. In Proceedings of IFIP Congress, 1983, 321--332.Google Scholar
- Jung, R. Jourdan, J.-H., Krebbers, R. and Dreyer. D. RustBelt: Securing the foundations of the Rust programming language. In Proceedings of PACMPL, 2018. Google ScholarDigital Library
- Krebbers, R., Jung, R., Bizjak, A., Jourdan, J-H, Dreyer, D. and Birkedal, L. The essence of higher-order concurrent separation logic. In Proceedings of ESOP, 2017, 696--723. Google ScholarDigital Library
- O'Hearn, P.W. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1--3 (2007), 271--307. Google ScholarDigital Library
- O'Hearn, P.W and Pym, D.J. The logic of bunched implications. Bulletin of Symbolic Logic 5, 2 (1999), 215--244.Google ScholarCross Ref
- O'Hearn, P.W., Reynolds, J.C. and Yang, H. Local reasoning about programs that alter data structures. In Proceedings of CSL, 2001, 1--19. Google ScholarDigital Library
- Parkinson. M.J. Local reasoning for Java. Ph.D. thesis. University of Cambridge, U.K., 2005.Google Scholar
- Parkinson, M.J., Bornat, R. and Calcagno, C. Variables as resource in Hoare logics. In Proceedings of 21<sup>st</sup> LIC, 2006, 137--146. Google ScholarDigital Library
- Philippaerts, P., Mühlberg, J.T., Penninckx, W., Smans, J., Jacobs, B. and Piessens, F. Software verification with verifast: Industrial case studies. Sci. Comput. Program. 82 (2014), 77--97. Google ScholarDigital Library
- Pym, D., O'Hearn, P. and Yang, H. Possible worlds and resources: The semantics of BI. Theoret. Comp. Sci. 315, 1 (2004), 257--305. Google ScholarDigital Library
- Reynolds, J,C. Intuitionistic reasoning about shared mutable data structure. Millennial Perspectives in Computer Science, Cornerstones of Computing. Palgrave Macmillan, 2000.Google Scholar
- Reynolds, J.C. Separation logic: A logic for shared mutable data structures. LICS, 2002, 55--74. Google ScholarDigital Library
- Sergey, I., Nanevski, A. and Banerjee, A. Mechanized verification of fine-grained concurrent programs. In Proceedings of 36<sup>th</sup> PLDI, 2015, 77--87. Google ScholarDigital Library
- Turing, A.M. Checking a large routine. Report of a Conference on High-Speed Automatic Calculating Machines. Univ. Math. Lab., Cambridge, U.K., 1949, 67--69.Google Scholar
- Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H. and Li, Z. A practical verification framework for preemptive OS kernels. In Proceedings of CAV, 2016.Google ScholarCross Ref
- Yang, H. Local Reasoning for Stateful Programs. Ph.D. thesis. University of Illinois, 2001. Google ScholarDigital Library
- Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D. and O'Hearn, P.W. Scalable shape analysis for systems code. In Proceedings of CAV, 2008, 385--398. Google ScholarDigital Library
- Yang, H. and O'Hearn, P.W. A semantic basis for local reasoning. In Proceedings of FoSSaCS, 2002, 402--416. Google ScholarDigital Library
Index Terms
- Separation logic
Recommendations
Translating Separation Logic into a Fragment of the First-Order Logic
SKG '10: Proceedings of the 2010 Sixth International Conference on Semantics, Knowledge and GridsSeparation logic is an extension of Hoare logic for reasoning about mutable heap structure. To represent separation logic in the first-order logic, there are several choices to determine what are constants, what are predicates and quantifiers, and ...
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Comments