Completeness and expressiveness of pointer program verification by separation logic

Ameen, 2016, Completeness for recursive procedures in separation logic, Theor. Comput. Sci., 631, 73, 10.1016/j.tcs.2016.04.004 Apt, 1981, Ten years of Hoare's logic: a survey — part I, ACM Trans. Program. Lang. Syst., 3, 431, 10.1145/357146.357150 Berdine, 2005, Symbolic execution with separation logic, vol. 3780, 52 Bergstra, 1982, Expressiveness and the completeness of Hoare's logic, J. Comput. Syst. Sci., 25, 267, 10.1016/0022-0000(82)90013-7 Brotherston, 2007, Formalised inductive reasoning in the logic of bunched implications, vol. 4634, 87 Brotherston, 2008, Cyclic proofs of program termination in separation logic, 101 Brotherston, 2011, Automated cyclic entailment proofs in separation logic, vol. 6803, 131 Calcagno, 2005, From separation logic to first-order logic, vol. 3441, 395 Calcagno, 2007, Context logic as modal logic: completeness and parametric inexpressivity, 123 Chin, 2012, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Sci. Comput. Program., 77, 1006, 10.1016/j.scico.2010.07.004 Cook, 1978, Soundness and completeness of an axiom system for program verification, SIAM J. Comput., 7, 70, 10.1137/0207005 Coquand, 1990, Inductively defined types, vol. 417, 50 Gulwani, 2008, Lifting abstract interpreters to quantified logical domains, 235 Halpern, 1984, A good Hoare axiom system for an ALGOL-like language, 262 Ishtiaq, 2001, BI as an assertion language for mutable data structures, 14 Josko, 1984, On expressive interpretations of a Hoare-logic for Clarke's language L4, vol. 166, 73 Kimura, 2013, Call-by-value and call-by-name dual calculi with inductive and coinductive types, Log. Methods Comput. Sci., 9 Kong, 2010, Automatically inferring quantified loop invariants by algorithmic learning from simple templates, vol. 6461, 328 Lozes, 2005, Elimination of spatial connectives in static spatial logics, Theor. Comput. Sci., 330, 475, 10.1016/j.tcs.2004.10.006 Nguyen, 2007, Automated verification of shape and size properties via separation logic, vol. 4349, 251 Nguyen, 2008, Enhancing program verification with lemmas, vol. 5123, 355 Paulin-Mohring, 1989, Extracting Fω's programs from proofs in the calculus of constructions, 89 Pohlers, 2009 Reynolds, 2002, Separation logic: a logic for shared mutable data structures, 55 Tatsuta, 1991, Program synthesis using realizability, Theor. Comput. Sci., 90, 309 Tatsuta, 2009, Completeness of pointer program verification by separation logic, 179 Tatsuta, 2014, Completeness of separation logic with inductive definitions for program verification, vol. 8702, 20 Weber, 2004, Towards mechanized program verification with separation logic, vol. 3210, 250