1: \begin{thebibliography}{10}
2:
3: \bibitem{BaaderETAL03DescriptionLogicHandbook}
4: Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter
5: Patel-Schneider, editors.
6: \newblock {\em The Description Logic Handbook: Theory, Implementation and
7: Applications}.
8: \newblock Cambridge University Press, 2003.
9:
10: \bibitem{BackETAL03ReasoningPointersRefinementCalculus}
11: Ralph-Johan Back, Xiaocong Fan, and Viorel Preoteasa.
12: \newblock Reasoning about pointers in refinement calculus.
13: \newblock In {\em 10th Asia-Pacific Software Engineering Conference
14: (APSEC'03)}, 2003.
15:
16: \bibitem{BackWright98RefinementCalculus}
17: Ralph-Johan Back and Joakim von Wright.
18: \newblock {\em Refinement Calculus}.
19: \newblock Springer-Verlag, 1998.
20:
21: \bibitem{Barendregt84LambdaCalculus}
22: Henk~P. Barendregt.
23: \newblock {\em The Lambda-Calculus: Its Syntax and Semantics}.
24: \newblock North-Holland, 2nd edition, 1984.
25:
26: \bibitem{Barendregt01LambdaCalculiTypes}
27: Henk~P. Barendregt.
28: \newblock Lambda calculi with types.
29: \newblock In {\em Handbook of Logic in Computer Science, Vol. II}. Oxford
30: University Press, 2001.
31:
32: \bibitem{BenediktETAL98VerifiablePropertiesDatabaseTransactions}
33: Michael Benedikt, Timothy Griffin, and Leonid Libkin.
34: \newblock Verifiable properties of database transactions.
35: \newblock {\em Information and Computation}, 147:57--88, 1998.
36:
37: \bibitem{BenediktETAL99LogicForLinked}
38: Michael Benedikt, Thomas Reps, and Mooly Sagiv.
39: \newblock A decidable logic for linked data structures.
40: \newblock In {\em Proc. 8th ESOP}, 1999.
41:
42: \bibitem{BoergerStaerk03AbstractStateMachines}
43: Egon B\"orger and Robert St\"ark.
44: \newblock {\em Abstract State Machines}.
45: \newblock Springer-Verlag, 2003.
46:
47: \bibitem{Borgida95DescriptionLogicsDataManagement}
48: Alexander Borgida.
49: \newblock Description logics in data management.
50: \newblock {\em IEEE Trans. on Knowledge and Data Engineering}, 7(5):671--682,
51: 1995.
52:
53: \bibitem{Borgida96RelativeExpressivenessDescriptionLogicsPredicateLogics}
54: Alexander Borgida.
55: \newblock Description logics in data management.
56: \newblock {\em Artificial Intelligence}, 82(1-2):353--367, 1996.
57:
58: \bibitem{CalcagnoETAL02DecidingValiditySpatialLogicTrees}
59: Cristiano Calcagno, Luca Cardelli, and Andrew~D. Gordon.
60: \newblock Deciding validity in a spatial logic for trees.
61: \newblock In {\em ACM TLDI'02}, 2002.
62:
63: \bibitem{CalcagnoETAL00SemanticAnalysisPointerAliasings}
64: Cristiano Calcagno, Samin Ishtiaq, and Peter~W. O'Hearn.
65: \newblock Semantic analysis of pointer aliasing, allocation and disposal in
66: hoare logic.
67: \newblock In {\em Proc. 2nd International Conference on Principles and Practice
68: of Declarative Programming}, 2000.
69:
70: \bibitem{Calvanese96FiniteModelReasoningDescriptionLogics}
71: Diego Calvanese.
72: \newblock Finite model reasoning in description logics.
73: \newblock In {\em Proc. of the 5th Int. Conf. on the Principles of Knowledge
74: Representation and Reasoning (KR'96)}, pages 292--303. Morgan Kaufmann, 1996.
75:
76: \bibitem{Calvanese96UnrestrictedFiniteModelReasoning}
77: Diego Calvanese.
78: \newblock {\em Unrestricted and Finite Model Reasoning in Class-Based
79: Representation Formalisms}.
80: \newblock PhD thesis, Dipartimento di Informatica e Sistemistica, Universita di
81: Roma "La Sapienza", 1996.
82:
83: \bibitem{ChaseETAL90AnalysisPointersStructures}
84: David~R. Chase, Mark Wegman, and F.~Kenneth Zadeck.
85: \newblock Analysis of pointers and structures.
86: \newblock In {\em Proc. ACM PLDI}, 1990.
87:
88: \bibitem{Chen76EntityRelationshipModel}
89: Peter Pin-Shan Chen.
90: \newblock The entity-relationship model--toward a unified view of data.
91: \newblock {\em ACM Transactions on Database Systems (TODS)}, 1(1):9--36, 1976.
92:
93: \bibitem{ChongRugina03StaticAnalysisAccessedRegionsRecursiveDataStructures}
94: Stephen Chong and Radu Rugina.
95: \newblock Static analysis of accessed regions in recursive data structures.
96: \newblock In {\em Proc. 10th SAS}, volume 2694 of {\em LNCS}. Springer, 2003.
97:
98: \bibitem{Codd70RelationalModelDataLargeSharedDataBanks}
99: Edgar~F. Codd.
100: \newblock A relational model of data for large shared data banks.
101: \newblock {\em CACM}, 13(6):377--387, 1970.
102:
103: \bibitem{CousotCousot77AbstractInterpretation}
104: Patrick Cousot and Radhia Cousot.
105: \newblock Abstract interpretation: a unified lattice model for static analysis
106: of programs by construction or approximation of fixpoints.
107: \newblock In {\em Proc. 4th POPL}, 1977.
108:
109: \bibitem{CousotCousot77RecursiveProcedures}
110: Patrick Cousot and Radhia Cousot.
111: \newblock Static determination of dynamic properties of recursive procedures.
112: \newblock In E.J{.} Neuhold, editor, {\em IFIP Conf{.} on Formal Description of
113: Programming Concepts, St-Andrews, N.B., CA}, pages 237--277.
114: North\discretionary{-}{}{-}Holland, 1977.
115:
116: \bibitem{CousotCousot79SystematicDesignProgramAnalysis}
117: Patrick Cousot and Radhia Cousot.
118: \newblock Systematic design of program analysis frameworks.
119: \newblock In {\em Proc. 6th POPL}, pages 269--282, San Antonio, Texas, 1979.
120: ACM Press, New York, NY.
121:
122: \bibitem{Bruijn72LambdaCalculusNotationNamelessDummies}
123: N.~G. de~Bruijn.
124: \newblock Lambda calculus notation with nameless dummies, a tool for automatic
125: formula manipulation, with application to the {C}hurch-{R}osser theorem.
126: \newblock {\em Indag. Math.}, 34:381--392, 1972.
127:
128: \bibitem{FlanaganETAL02ExtendedStaticCheckingJava}
129: Cormac Flanagan, K.~Rustan~M. Leino, Mark Lilibridge, Greg Nelson, James~B.
130: Saxe, and Raymie Stata.
131: \newblock {E}xtended {S}tatic {C}hecking for {J}ava.
132: \newblock In {\em Proc. ACM PLDI}, 2002.
133:
134: \bibitem{Floyd67AssigningMeaningsPrograms}
135: Robert~W. Floyd.
136: \newblock Assigning meanings to programs.
137: \newblock In {\em Proc. Amer. Math. Soc. Symposia in Applied Mathematics},
138: volume~19, pages 19--31, 1967.
139:
140: \bibitem{FradetETALStaticVerificationPointer}
141: Pascal Fradet, Ronan Gaugne, and Daniel~Le Metayer.
142: \newblock An inference algorithm for the static verification of pointer
143: manipulation.
144: \newblock Technical Report 980, IRISA, 1996.
145:
146: \bibitem{FradetMetayer97ShapeTypes}
147: Pascal Fradet and Daniel~Le M\'etayer.
148: \newblock Shape types.
149: \newblock In {\em Proc. 24th ACM POPL}, 1997.
150:
151: \bibitem{FradetMetayer98StructuredGamma}
152: Pascal Fradet and Daniel~Le M\'etayer.
153: \newblock Structured gamma.
154: \newblock {\em Science of Computer Programming, SCP, 31(2-3), pp. 263-289},
155: 1998.
156:
157: \bibitem{GaugneETAL96StaticDetectionPointerErrors}
158: R.~Gaugne, P.~Fradet, and D.~Le M\'etayer.
159: \newblock Static detection of pointer errors: an axiomatisation and a checking
160: algorithm.
161: \newblock In {\em Proc. European Symposium on Programming, ESOP'96}, LNCS,
162: 1996.
163:
164: \bibitem{GhiyaHendren96TreeOrDag}
165: Rakesh Ghiya and Laurie Hendren.
166: \newblock Is it a tree, a {DAG}, or a cyclic graph?
167: \newblock In {\em Proc. 23rd ACM POPL}, 1996.
168:
169: \bibitem{GraedelETAL97TwoVariableLogicCountingDecidable}
170: Erich Gr{\"a}del, Martin Otto, and Eric Rosen.
171: \newblock Two-variable logic with counting is decidable.
172: \newblock In {\em Proceedings of 12th IEEE Symposium on Logic in Computer
173: Science LICS `97, Warschau}, 1997.
174:
175: \bibitem{HarelETAL00DynamicLogic}
176: David Harel, Dexter Kozen, and Jerzy Tiuryn.
177: \newblock {\em Dynamic Logic}.
178: \newblock The MIT Press, Cambridge, Mass., 2000.
179:
180: \bibitem{Hoare69AxiomaticBasisComputerProgramming}
181: C.~A.~R. Hoare.
182: \newblock An axiomatic basis for computer programming.
183: \newblock {\em Communications of the ACM}, 12(10):576--580, 1969.
184:
185: \bibitem{HummelETAL94GeneralDataDependence}
186: Joseph Hummel, Laurie~J. Hendren, and Alexandru Nicolau.
187: \newblock A general data dependence test for dynamic, pointer-based data
188: structures.
189: \newblock In {\em Proc. ACM PLDI}, 1994.
190:
191: \bibitem{IshtiaqOHearn01BIAssertionLanguage}
192: Samin Ishtiaq and Peter~W. O'Hearn.
193: \newblock {BI} as an assertion language for mutable data structures.
194: \newblock In {\em Proc. 28th ACM POPL}, 2001.
195:
196: \bibitem{Jackson01OMInvariants}
197: Daniel Jackson.
198: \newblock Object models as heap invariants.
199: \newblock In Annabelle McIver and Carroll Morgan, editors, {\em Collected
200: Papers of IFIP Working Group 2.3 on Programming Methodology}.
201: Springer-Verlag, 2001.
202:
203: \bibitem{Jackson02AlloyTOSEM}
204: Daniel Jackson.
205: \newblock Alloy: a lightweight object modelling notation.
206: \newblock {\em ACM TOSEM}, 11(2):256--290, 2002.
207:
208: \bibitem{JensenETAL97MonadicLogic}
209: Jacob~L. Jensen, Michael~E. J{\o}rgensen, Nils Klarlund, and Michael~I.
210: Schwartzbach.
211: \newblock Automatic verification of pointer programs using monadic second order
212: logic.
213: \newblock In {\em Proc. ACM PLDI}, Las Vegas, NV, 1997.
214:
215: \bibitem{Jones87ImplementationFunctionalProgrammingLanguages}
216: Simon L.~Peyton Jones.
217: \newblock {\em The Implementation of Functional Programming Languages}.
218: \newblock Prentice-Hall, 1987.
219:
220: \bibitem{KlarlundSchwartzbach93GraphTypes}
221: Nils Klarlund and Michael~I. Schwartzbach.
222: \newblock Graph types.
223: \newblock In {\em Proc. 20th ACM POPL}, Charleston, SC, 1993.
224:
225: \bibitem{KlarlundSchwartzbach94Transductions}
226: Nils Klarlund and Michael~I. Schwartzbach.
227: \newblock Graphs and decidable transductions based on edge constraints.
228: \newblock In {\em Proc. 19th Colloquium on Trees and Algebra in Programming},
229: number 787 in LNCS, 1994.
230:
231: \bibitem{Kowalski79AlgorithmLogicControl}
232: Robert Kowalski.
233: \newblock Algorithm = logic + control.
234: \newblock {\em Communications of the ACM}, 1979.
235:
236: \bibitem{Kuncak01DesigningRoleAnalysis}
237: Viktor Kuncak.
238: \newblock Designing an algorithm for role analysis.
239: \newblock Master's thesis, MIT Laboratory for Computer Science, 2001.
240:
241: \bibitem{KuncakETAL02RoleAnalysis}
242: Viktor Kuncak, Patrick Lam, and Martin Rinard.
243: \newblock Role analysis.
244: \newblock In {\em Proc. 29th POPL}, 2002.
245:
246: \bibitem{KuncakLeino03InPlaceRefinementEffectChecking}
247: Viktor Kuncak and K.~Rustan~M. Leino.
248: \newblock In-place refinement for effect checking.
249: \newblock In {\em Second International Workshop on Automated Verification of
250: Infinite-State Systems (AVIS'03), Warsaw, Poland}, April 2003.
251:
252: \bibitem{KuncakRinard01ObjectModelsHeapsInterpretations}
253: Viktor Kuncak and Martin Rinard.
254: \newblock Object models, heaps, and interpretations.
255: \newblock Technical Report 816, MIT Laboratory for Computer Science, January
256: 2001.
257:
258: \bibitem{KuncakRinard02TypestateCheckingRegularGraphConstraints}
259: Viktor Kuncak and Martin Rinard.
260: \newblock Typestate checking and regular graph constraints.
261: \newblock Technical Report 863, MIT Laboratory for Computer Science, 2002.
262:
263: \bibitem{KuncakRinard03ExistentialHeapAbstractionEntailment}
264: Viktor Kuncak and Martin Rinard.
265: \newblock Existential heap abstraction entailment is undecidable.
266: \newblock In {\em 10th Annual International Static Analysis Symposium (SAS
267: 2003)}, San Diego, California, June 11-13 2003.
268:
269: \bibitem{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints}
270: Viktor Kuncak and Martin Rinard.
271: \newblock On the boolean algebra of shape analysis constraints.
272: \newblock Technical report, MIT CSAIL, August 2003.
273:
274: \bibitem{KuncakRinard03TheoryStructuralSubtyping}
275: Viktor Kuncak and Martin Rinard.
276: \newblock On the theory of structural subtyping.
277: \newblock Technical Report 879, Laboratory for Computer Science, Massachusetts
278: Institute of Technology, 2003.
279:
280: \bibitem{LeinoETAL02DataGroupsSideEffects}
281: K.~Rustan~M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou.
282: \newblock Using data groups to specify and check side effects.
283: \newblock In {\em Proc. ACM PLDI}, 2002.
284:
285: \bibitem{LenzeriniNobili87SatisfiabilityDependencyConstraintsER}
286: Maurizio Lenzerini and Paolo Nobili.
287: \newblock On the satisfiability of dependency constraints in
288: entity-relationship schemata.
289: \newblock In {\em Proc. 13th VLDB}, pages 147--154, 1987.
290:
291: \bibitem{LevAmiETAL00PuttingStaticAnalysisWorkVerification}
292: Tal Lev-Ami, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm.
293: \newblock Putting static analysis to work for verification: A case study.
294: \newblock In {\em International Symposium on Software Testing and Analysis},
295: 2000.
296:
297: \bibitem{Lloyd87FoundationsLogicProgramming}
298: John~W. Lloyd.
299: \newblock {\em Foundations of Logic Programming}.
300: \newblock Springer-Verlag, 2nd edition, 1987.
301:
302: \bibitem{MehtaNipkow03ProvingPointerProgramsHigherOrderLogic}
303: Farhad Mehta and Tobias Nipkow.
304: \newblock Proving pointer programs in higher-order logic.
305: \newblock In F.~Baader, editor, {\em Automated Deduction --- CADE-19}, LNCS.
306: Springer-Verlag, 2003.
307:
308: \bibitem{Moeller01PALE}
309: Anders M{\o}ller and Michael~I. Schwartzbach.
310: \newblock The {P}ointer {A}ssertion {L}ogic {E}ngine.
311: \newblock In {\em Proc. ACM PLDI}, 2001.
312:
313: \bibitem{Morgan94ProgrammingFromSpecifications}
314: Carroll Morgan.
315: \newblock {\em Programming from Specifications (2nd ed.)}.
316: \newblock Prentice-Hall, Inc., 1994.
317:
318: \bibitem{PacholskiETAL00ComplexityResultsFirstOrderTwo}
319: Leszek Pacholski, Wieslaw Szwast, and Lidia Tendera.
320: \newblock Complexity results for first-order two-variable logic with counting.
321: \newblock {\em SIAM J. on Computing}, 29(4):1083--1117, 2000.
322:
323: \bibitem{Paulson94Isabelle}
324: Lawrence~C. Paulson.
325: \newblock {\em Isabelle: A Generic Theorem Prover}.
326: \newblock Number 828 in LNCS. Springer-Verlag, 1994.
327:
328: \bibitem{Reynolds00IntuitionisticReasoningMutable}
329: John~C. Reynolds.
330: \newblock Intuitionistic reasoning about shared mutable data structure.
331: \newblock In {\em Proceedings of the Symposium in Celebration of the Work of
332: C.A.R. Hoare}, 2000.
333:
334: \bibitem{Reynolds02SeparationLogic}
335: John~C. Reynolds.
336: \newblock Separation logic: a logic for shared mutable data structures.
337: \newblock In {\em 17th LICS}, pages 55--74, 2002.
338:
339: \bibitem{RinetzkySagiv01InterprocedualShapeAnalysis}
340: Noam Rinetzky and Mooly Sagiv.
341: \newblock Interprocedual shape analysis for recursive programs.
342: \newblock In {\em Proc. 10th International Conference on Compiler
343: Construction}, 2001.
344:
345: \bibitem{Rozenberg97HandbookGraphGrammars}
346: Grzegorz Rozenberg, editor.
347: \newblock {\em Handbook of Graph Grammars and Computing by Graph
348: Transformations Vol.1}.
349: \newblock World Scientific, 1997.
350:
351: \bibitem{RumbaughETAL99UMLReference}
352: James Rumbaugh, Ivar Jacobson, and Grady Booch.
353: \newblock {\em The Unified Modelling Language Reference Manual}.
354: \newblock Addison-Wesley, Reading, Mass., 1999.
355:
356: \bibitem{SagivETAL99Parametric}
357: Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
358: \newblock Parametric shape analysis via 3-valued logic.
359: \newblock In {\em Proc. 26th ACM POPL}, 1999.
360:
361: \bibitem{SagivETAL02Parametric}
362: Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
363: \newblock Parametric shape analysis via 3-valued logic.
364: \newblock {\em ACM TOPLAS}, 24(3):217--298, 2002.
365:
366: \bibitem{SchonbergETAL91Setl}
367: E.~Schonberg, J.~T. Schwartz, and M.~Sharir.
368: \newblock An automatic technique for selection of data representations in
369: {S}etl programs.
370: \newblock {\em Transactions on Programming Languages and Systems},
371: 3(2):126--143, 1991.
372:
373: \bibitem{Skolem19Untersuchungen}
374: Thoralf Skolem.
375: \newblock Untersuchungen \"uber die {A}xiome des {K}lassenkalk\"uls and \"uber
376: ``{P}roduktations- und {S}ummationsprobleme'', welche gewisse {K}lassen von
377: {A}ussagen betreffen.
378: \newblock Skrifter utgit av {V}idnskapsselskapet i {K}ristiania, I. klasse, no.
379: 3, {O}slo, 1919.
380:
381: \bibitem{WhaleyRinard99CompositionalPointerEscapeAnalysis}
382: J.~Whaley and M.~Rinard.
383: \newblock Compositional pointer and escape analysis for {J}ava programs.
384: \newblock In {\em Proc. 14th Annual ACM Conference on Object-Oriented
385: Programming, Systems, Languages, and Applications}, Denver, November 1999.
386:
387: \bibitem{WilsonLam95PointerAnalysis}
388: R.~Wilson and M.~S. Lam.
389: \newblock Efficient context-sensitive pointer analysis for {C} programs.
390: \newblock In {\em Proc. ACM PLDI}, June 1995.
391:
392: \bibitem{YiHarrison93AutomaticGenerationInterproceduralAnalyses}
393: Kwangkeun Yi and Williams~Ludwell {Harrison III}.
394: \newblock Automatic generation and management of interprocedural program
395: analyses.
396: \newblock In {\em 20th ACM POPL}, 1993.
397:
398: \bibitem{Yorsh03LogicalCharacterizationsHeapAbstractions}
399: Greta Yorsh.
400: \newblock Logical characterizations of heap abstractions.
401: \newblock Master's thesis, Tel-Aviv University, March 2003.
402:
403: \end{thebibliography}
404: