Symbolic Execution Proofs for Higher Order Store Programs

详细信息    查看全文

• 作者：Bernhard Reus (1)
  Nathaniel Charlton (1)
  Ben Horsfall (1)
  
• 关键词：Program verification ; Higher order store ; Recursion through the store ; Separation logic ; Automated verification
• 刊名：Journal of Automated Reasoning
• 出版年：2015
• 出版时间：March 2015
• 年：2015
• 卷：54
• 期：3
• 页码：199-284
• 全文大小：6,390 KB
• 参考文献：1. The Crowfoot website. www.sussex.ac.uk/informatics/crowfoot (2011)
  2. Beckmann, O., Houghton, A., Mellor, M.R., Kelly, P.H.J.: Runtime code generation in C++ as a foundation for domain-specific optimisation. In: Domain-Specific Program Generation, pp 291鈥?06 (2003)
  3. Benton, N., Kennedy, A., Beringer, L., Hofmann, M.: Relational semantics for effect-based program transformations: higher-order store. In: PPDP, pp 301鈥?12 (2009)
  4. Berdine, J., Calcagno, C., O鈥橦earn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: FMCO, pp 115鈥?37 (2005)
  5. Berdine, J., Calcagno, C., O鈥橦earn, P.W.: Symbolic execution with separation logic. In: APLAS, pp 52鈥?8 (2005)
  6. Biering, B., Birkedal, L., Torp-Smith, N. : Bi-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst. 29 (5) (2007)
  7. Birkedal, L., Reus, B., Schwinghammer, J., St酶vring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL鈥?1, pp 119鈥?32. IEEE (2011)
  8. Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for Algol-like languages. LMCS 2 (5) (2006)
  9. Blom, S., Huisman, M.: Witnessing the elimination of magic wands (2013)
  10. Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: PLDI, pp 66鈥?7 (2007)
  11. Calcagno, C., Distefano, D., O鈥橦earn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. ACM SIGPLAN Notices 44 (1), 289鈥?00 (2009) CrossRef
  12. Chargu茅raud, A: Characteristic formulae for the verification of imperative programs. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP, pp 418鈥?30. ACM (2011)
  13. Charlton, N., Horsfall, B., Reus, B.: Formal reasoning about runtime code update. In: Abiteboul, S., B枚hm, K., Koch, C., Tan, K.-L. (eds.) ICDE Workshops, pp 134鈥?38. IEEE (2011)
  14. Charlton, N., Horsfall, B., Reus, B. : Crowfoot: A verifier for higher-order store programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI, volume 7148 of Lecture Notes in Computer Science, pp 136鈥?51. Springer (2012)
  15. Charlton, N., Reus, B.: A deeper understanding of the deep frame axiom. Extended abstract, presented at LOLA (Syntax and Semantics of Low Level Languages) (2010)
  16. Charlton, N., Reus, B.: Specification patterns and proofs for recursion through the store. In: FCT, pp 310鈥?21 (2011)
  17. Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77 (9), 1006鈥?036 (2012) CrossRef
  18. Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp 234鈥?45. ACM (2011)
  19. 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, pp 79鈥?0. ACM (2009)
  20. Distefano, D., O鈥橦earn, P.W., Yang, H.: A local shape analysis based on separation logic. In: TACAS, pp 287鈥?02 (2006)
  21. Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA, pp 213鈥?26 (2008)
  22. Gherghina, C., David, C., Qin, S., Chin, W.-N.: Structured specifications for better verification of heap-manipulating programs. In: FM, pp 386鈥?01 (2011)
  23. Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer (1979)
  24. Henderson, B.: Linux loadable kernel module HOWTO (v1.09). Available online http://tldp.org/HOWTO/Module-HOWTO/ (2006)
  25. Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pp 102鈥?16. Springer Berlin, Heidelberg (1971) CrossRef
  26. Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS, pp 270鈥?79 (2005)
  27. Horsfall, B.: Automated reasoning for reflective programs. PhD thesis (2014)
  28. Horsfall, B., Charlton, N., Reus, B.: Verifying the reflective visitor pattern. In: FtFJP, pp 27鈥?4 (2012)
  29. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: NASA Formal Methods, pp 41鈥?5 (2011)
  30. Jacobs, B, Smans, J, Piessens, F: A quick tour of the VeriFast program verifier. In: APLAS, pp 304鈥?11 (2010)
  31. Lee, W., Park, S.: A proof system for separation logic with magic wand. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pp. 477鈥?90, New York, USA, 2014. ACM
  32. Nanevski, A. J., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18 (5鈥?), 865鈥?11 (2008) CrossRef
  33. Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL, pp 320鈥?33 (2006)
  34. Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In LICS, pp. 331鈥?40, Pittsburgh, Pennsylvania (2008)
  35. Pym, D.J., O鈥橦earn, P.W., Yang, H.: Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315 (1), 257鈥?05 (2004) CrossRef
  36. Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: CSL, pp 575鈥?90 (2006)
  37. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp 55鈥?4 (2002)
  38. Rutten, J.J.M.M.: Elements of generalized ultrametric domain theory. Theor. Comput. Sci. 170 (1鈥?), 349鈥?81 (1996) CrossRef
  39. Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. Technical report, ETH Zurich (2014)
  40. Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and frame rules for higher-order store. In: CSL, pp 440鈥?54 (2009)
  41. Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and frame rule for higher-order store. Logical Methods Comput. Sci. 7 (3) (2011)
  42. Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., Reus, B: A semantic foundation for hidden state. In: FOSSACS, pp 2鈥?7 (2010)
  43. Stoyle, G., Hicks, M., Bierman, G., Sewell, P., Neamtiu, I.: Mutatis mutandis: Safe and predictable dynamic software updating. ACM Trans. Program. Lang. Syst. 29 (4) (2007)
  
• 作者单位：Bernhard Reus (1)
  Nathaniel Charlton (1)
  Ben Horsfall (1)
  
  1. Department of Informatics, University of Sussex, Brighton, United Kingdom
  
• 刊物类别：Computer Science
• 刊物主题：Mathematical Logic and Formal Languages
  Artificial Intelligence and Robotics
  Mathematical Logic and Foundations
  Symbolic and Algebraic Manipulation
  
• 出版者：Springer Netherlands
• ISSN：1573-0670

文摘

Higher order store programs are programs which store, manipulate and invoke code at runtime. Important examples of higher order store programs include operating system kernels which dynamically load and unload kernel modules. Yet conventional Hoare logics, which provide no means of representing changes to code at runtime, are not applicable to such programs. Recently, however, new logics using nested Hoare triples have addressed this shortcoming. In this paper we describe, from top to bottom, a sound semi-automated verification system for higher order store programs. We give a programming language with higher order store features, define an assertion language with nested triples for specifying such programs, and provide reasoning rules for proving programs correct. We then present in full our algorithms for automatically constructing correctness proofs. In contrast to earlier work, the language also includes ordinary (fixed) procedures and mutable local variables, making it easy to model programs which perform dynamic loading and other higher order store operations. We give an operational semantics for programs and a step-indexed interpretation of assertions, and use these to show soundness of our reasoning rules, which include a deep frame rule which allows more modular proofs. Our automated reasoning algorithms include a scheme for separation logic based symbolic execution of programs, and automated provers for solving various kinds of entailment problems. The latter are presented in the form of sets of derived proof rules which are constrained enough to be read as a proof search algorithm.