Reasoning about Assignments in Recursive Data Structures - Formal Methods: Foundations and Applications - page 176

3. Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R.,
Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102-126. Springer, Heidelberg
(2000)
4. Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: meta-level guidance for
mathematical reasoning. Cambridge University Press, Cambridge (2005)
5. Burstall, R.: Some techniques for proving correctness of programs which alter data
structures. In: Machine Intelligence, vol. 7, pp. 22-50. Edinburgh University Press
(1972)
6. Distefano, D., Filipović, I.: Memory leaks detection in Java by bi-abductive in-
ference. In: Rosenblum, D., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp.
278-292. Springer, Heidelberg (2010)
7. Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deduc-
tive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS,
vol. 4590, pp. 173-177. Springer, Heidelberg (2007)
8. Hoare, C.A.R., Jifeng, H.: A trace model for pointers and objects. In: Guerraoui, R.
(ed.) ECOOP 1999. LNCS, vol. 1628, pp. 1-17. Springer, Heidelberg (1999)
9. Hubert, T., Marché, C.: Separation analysis for deductive verification. In:
Damm, W., Hermanns, H. (eds.) HAV 2007: Heap Analysis and Verification, Braga,
Portugal, pp. 81-93 (2007)
10. Marché, C., Paulin-Mohring, C.: Reasoning about Java programs with aliasing and
frame conditions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603,
pp. 179-194. Springer, Heidelberg (2005)
11. Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information
and Computation 199, 200-227 (2005)
12. Meyer, B.: Towards practical proofs of class correctness. In: Bert, D., Bowen, J.P.,
King, S., Waldén, M. (eds.) ZB 2003. LNCS, vol. 2651, pp. 359-387. Springer,
Heidelberg (2003)
13. Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS language reference
(version 2.4). Technical report, Computer Science Laboratory, SRI International
(2001)
14. Reynolds, J.: Separation logic: A logic for shared mutable data structures. In:
LICS 2002: Logic in Computer Science, pp. 55-74. IEEE Computer Society,
Los Alamitos (2002)
15. Rosenberg, S., Banerjee, A., Naumann, D.A.: Local reasoning and dynamic framing
for the composite pattern and its clients (to appear)
16. Tamalet, A.: Yet another semantics for proving class correctness. Master's thesis,
Universidad Nacional de Rosario, Argentina (2006)
17. Tuerk, T.: A formalisation of Smallfoot in HOL. In: Berghofer, S., Nipkow, T.,
Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469-484.
Springer, Heidelberg (2009)
18. von Henke, F.W., Pfab, S., Pfeifer, H., Rueß, H.: Case studies in meta-level theorem
proving. In: Grundy, J., Newey, M.C. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp.
461-478. Springer, Heidelberg (1998)