1: \begin{thebibliography}{10}
2:
3: \bibitem{AikenETAL03CheckingInferringLocalNonAliasing}
4: A.~Aiken, J.~S. Foster, J.~Kodumal, and T.~Terauchi.
5: \newblock Checking and inferring local non-aliasing.
6: \newblock In {\em PLDI 2003}, 2003.
7:
8: \bibitem{BarwiseFeferman85ModelTheoreticLogics}
9: J.~Barwise and S.~Feferman, editors.
10: \newblock {\em Model-Theoretic Logics}.
11: \newblock Springer, 1985.
12:
13: \bibitem{BenediktETAL99LogicForLinked}
14: M.~Benedikt, T.~Reps, and M.~Sagiv.
15: \newblock A decidable logic for linked data structures.
16: \newblock In {\em Proc. 8th ESOP}, 1999.
17:
18: \bibitem{BerdineETAL04DecidableFragmentSeparationLogic}
19: J.~Berdine, C.~Calcagno, and P.~O'Hearn.
20: \newblock A decidable fragment of separation logic.
21: \newblock In {\em FSTTCS}, 2004.
22:
23: \bibitem{BirkedalETAL04LocalReasoningCopyingCollector}
24: L.~Birkedal, N.~Torp-Smith, and J.~C. Reynolds.
25: \newblock Local reasoning about a copying garbage collector.
26: \newblock In {\em 31st ACM POPL}, pages 220--231. ACM Press, 2004.
27:
28: \bibitem{Blanchet98EscapeAnalysis}
29: B.~Blanchet.
30: \newblock Escape analysis: correctness proof, implementation and experimental
31: results.
32: \newblock In {\em Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on
33: Principles of programming languages}, pages 25--37. ACM Press, 1998.
34:
35: \bibitem{Blanchet03EscapeAnalysis}
36: B.~Blanchet.
37: \newblock Escape {A}nalysis for {J}ava({TM}). {T}heory and {P}ractice.
38: \newblock {\em ACM Transactions on Programming Languages and Systems}, 2003.
39: \newblock To appear.
40:
41: \bibitem{BoergerStaerk03AbstractStateMachines}
42: E.~B\"orger and R.~St\"ark.
43: \newblock {\em Abstract State Machines}.
44: \newblock Springer-Verlag, 2003.
45:
46: \bibitem{Burstall72SomeTechniquesProvingCorrectnessPrograms}
47: R.~Burstall.
48: \newblock Some techniques for proving correctness of programs which alter data
49: structures.
50: \newblock {\em Machine Intelligence}, 7, 1972.
51:
52: \bibitem{Caires04BehavioralSpatialObservationsLogicPiCalculus}
53: L.~Caires.
54: \newblock Behavioral and spatial observations in a logic for the pi-calculus.
55: \newblock In {\em FoSSaCS}, 2004.
56:
57: \bibitem{CairesCardelli03SpatialLogicConcurrencyPartI}
58: L.~Caires and L.~Cardelli.
59: \newblock A spatial logic for concurrency (part i).
60: \newblock {\em Information and Computation}, 186(2):194--235, 2003.
61:
62: \bibitem{CalcagnoETAL02DecidingValiditySpatialLogicTrees}
63: C.~Calcagno, L.~Cardelli, and A.~D. Gordon.
64: \newblock Deciding validity in a spatial logic for trees.
65: \newblock In {\em ACM TLDI'02}, 2002.
66:
67: \bibitem{CalcagnoETAL01ComputabilityComplexityResultsSpatialAssertion}
68: C.~Calcagno, H.~Yang, and P.~O'Hearn.
69: \newblock Computability and complexity results for a spatial assertion language
70: for data structures.
71: \newblock In {\em FSTTCS}, 2001.
72:
73: \bibitem{Ghelli02SpatialLogicMFPS}
74: L.~Cardelli, P.~Gardner, and G.~Ghelli.
75: \newblock A spatial logic for quering graphs.
76: \newblock Presentation at the 18th Workshop on Mathematical Foundations of
77: Programming Semantics, March 2002.
78:
79: \bibitem{LucaGhelli02SpatialLogicQueryingGraphs}
80: L.~Cardelli, P.~Gardner, and G.~Ghelli.
81: \newblock A spatial logic for querying graphs.
82: \newblock In {\em Proc. 29th ICALP}, volume 2380 of {\em LNCS}, 2002.
83:
84: \bibitem{CardelliGhelli01QueryLanguageAmbientLogic}
85: L.~Cardelli and G.~Ghelli.
86: \newblock A query language based on the ambient logic.
87: \newblock In {\em Proc. 10th ESOP}, volume 2028 of {\em LNCS}, 2001.
88:
89: \bibitem{CardelliGordon00AnytimeAnywhere}
90: L.~Cardelli and A.~D. Gordon.
91: \newblock Anytime, anywhere. modal logics for mobile ambients.
92: \newblock In {\em 27th ACM POPL}, 2000.
93:
94: \bibitem{ComonETAL97Tata}
95: H.~Comon, M.~Dauchet, R.~Gilleron, F.~Jacquemard, D.~Lugiez, S.~Tison, and
96: M.~Tommasi.
97: \newblock Tree automata techniques and applications.
98: \newblock Available on: {\tt http://www.grappa.univ-lille3.fr/tata}, 1997.
99: \newblock release 1999.
100:
101: \bibitem{CousotCousot79SystematicDesignProgramAnalysis}
102: P.~Cousot and R.~Cousot.
103: \newblock Systematic design of program analysis frameworks.
104: \newblock In {\em Proc. 6th POPL}, pages 269--282, San Antonio, Texas, 1979.
105: ACM Press, New York, NY.
106:
107: \bibitem{DawarETAL04ExpressivenessComplexityGraphLogic}
108: A.~Dawar, P.~Gardner, and G.~Ghelli.
109: \newblock Expressiveness and complexity of graph logic.
110: \newblock Technical Report~3, Imperial College, Department of Computing
111: Technical Report, 2004.
112:
113: \bibitem{DeLineFahndrich01EnforcingHighLevelProtocols}
114: R.~DeLine and M.~F\"ahndrich.
115: \newblock Enforcing high-level protocols in low-level software.
116: \newblock In {\em Proc. ACM PLDI}, 2001.
117:
118: \bibitem{FahndrichDeLine02AdoptionFocus}
119: M.~Fahndrich and R.~DeLine.
120: \newblock Adoption and focus: Practical linear types for imperative
121: programming.
122: \newblock In {\em Proc. ACM PLDI}, 2002.
123:
124: \bibitem{GraedelETAL97TwoVariableLogicCountingDecidable}
125: E.~Gr{\"a}del, M.~Otto, and E.~Rosen.
126: \newblock Two-variable logic with counting is decidable.
127: \newblock In {\em Proceedings of 12th IEEE Symposium on Logic in Computer
128: Science LICS `97, Warschau}, 1997.
129:
130: \bibitem{Hodges93ModelTheory}
131: W.~Hodges.
132: \newblock {\em Model Theory}, volume~42 of {\em Encyclopedia of Mathematics and
133: its Applications}.
134: \newblock Cambridge University Press, 1993.
135:
136: \bibitem{IshtiaqOHearn01BIAssertionLanguage}
137: S.~Ishtiaq and P.~W. O'Hearn.
138: \newblock {BI} as an assertion language for mutable data structures.
139: \newblock In {\em Proc. 28th ACM POPL}, 2001.
140:
141: \bibitem{KodumalAiken04SetConstraintCFLReachabilityConnection}
142: J.~Kodumal and A.~Aiken.
143: \newblock The set constraint/{CFL} reachability connection in practice.
144: \newblock In {\em Proc. ACM PLDI}, June 2004.
145:
146: \bibitem{KuncakETAL02RoleAnalysis}
147: V.~Kuncak, P.~Lam, and M.~Rinard.
148: \newblock Role analysis.
149: \newblock In {\em Proc. 29th POPL}, 2002.
150:
151: \bibitem{KuncakRinard03OnRoleLogic}
152: V.~Kuncak and M.~Rinard.
153: \newblock On role logic.
154: \newblock Technical Report 925, MIT CSAIL, 2003.
155:
156: \bibitem{KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable}
157: V.~Kuncak and M.~Rinard.
158: \newblock The first-order theory of sets with cardinality constraints is
159: decidable.
160: \newblock Technical Report 958, MIT CSAIL, July 2004.
161:
162: \bibitem{KuncakRinard04GeneralizedRecordsRoleLogic}
163: V.~Kuncak and M.~Rinard.
164: \newblock Generalized records and spatial conjunction in role logic.
165: \newblock In {\em 11th Annual International Static Analysis Symposium
166: (SAS'04)}, Verona, Italy, August 26--28 2004.
167:
168: \bibitem{KuncakRinard04OnRecordsSpatialConjunctionRoleLogic}
169: V.~Kuncak and M.~Rinard.
170: \newblock On generalized records and spatial conjunction in role logic.
171: \newblock Technical Report 942, MIT CSAIL, April 2004.
172:
173: \bibitem{LamETAL04OurExperienceModularPluggableAnalyses}
174: P.~Lam, V.~Kuncak, and M.~Rinard.
175: \newblock On our experience with modular pluggable analyses.
176: \newblock Technical Report 965, MIT CSAIL, September 2004.
177:
178: \bibitem{LamETAL04HobProjectWebPage}
179: P.~Lam, V.~Kuncak, K.~Zee, and M.~Rinard.
180: \newblock The {H}ob project web page.
181: \newblock http://catfish.csail.mit.edu/$\sim$plam/hob/, 2004.
182:
183: \bibitem{LevAmiETAL00PuttingStaticAnalysisWorkVerification}
184: T.~Lev-Ami, T.~Reps, M.~Sagiv, and R.~Wilhelm.
185: \newblock Putting static analysis to work for verification: A case study.
186: \newblock In {\em International Symposium on Software Testing and Analysis},
187: 2000.
188:
189: \bibitem{LozesCaires04EliminationQuantifiersUndecidabilitySpatialLogicsConcurr%
190: ency}
191: {\'E}.~Lozes and L.~Caires.
192: \newblock Elimination of quantifiers and undecidability in spatial logics for
193: concurrency.
194: \newblock In {\em CONCUR}, 2004.
195:
196: \bibitem{ManevichETAL02CompactlyRepresentingFirstOrderStructures}
197: R.~Manevich, G.~Ramalingam, J.~Field, D.~Goyal, and M.~Sagiv.
198: \newblock Compactly representing first-order structures for static analysis.
199: \newblock In {\em Proc. 9th International Static Analysis Symposium}, pages
200: 196--212, 2002.
201:
202: \bibitem{ManevichETAL04PartiallyDisjunctiveHeapAbstraction}
203: R.~Manevich, M.~Sagiv, G.~Ramalingam, and J.~Field.
204: \newblock Partially disjunctive heap abstraction.
205: \newblock In R.~Giacobazzi, editor, {\em Proceedings of the 11th International
206: Symposium, SAS 2004}, volume 3148 of {\em Lecture Notes in Computer Science},
207: pages 265--279. Springer, aug 2004.
208: \newblock Available at http://www.cs.tau.ac.il/$\sim$rumster/sas04.pdf.
209:
210: \bibitem{MelskiReps00InterconvertibilitySetConstraintsCFLReachability}
211: D.~Melski and T.~Reps.
212: \newblock Interconvertibility of a class of set constraints and context-free
213: language reachability.
214: \newblock {\em TCS}, 248:29--98, November 2000.
215:
216: \bibitem{Mendelson97IntroductionMathematicalLogic}
217: E.~Mendelson.
218: \newblock {\em Introduction to Mathematical Logic}.
219: \newblock Chapman \& Hall, London, 4th edition, 1997.
220:
221: \bibitem{Moeller01PALE}
222: A.~M{\o}ller and M.~I. Schwartzbach.
223: \newblock The {P}ointer {A}ssertion {L}ogic {E}ngine.
224: \newblock In {\em Proc. ACM PLDI}, 2001.
225:
226: \bibitem{NielsonETAL01KleenesLogicEquality}
227: F.~Nielson, H.~R. Nielson, and M.~Sagiv.
228: \newblock Kleene's logic with equality.
229: \newblock {\em Inf. Process. Lett.}, 80(3):131--137, 2001.
230:
231: \bibitem{OHearnPym99LogicBunchedImplications}
232: P.~O'Hearn and D.~Pym.
233: \newblock The logic of bunched implications.
234: \newblock {\em Bulleting of Symbolic Logic}, 5(2):215--244, 1999.
235:
236: \bibitem{OHearnETAL01LocalReasoning}
237: P.~O'Hearn, J.~Reynolds, and H.~Yang.
238: \newblock Local reasoning about programs that alter data structures.
239: \newblock In {\em Proc. CSL, Paris 2001}, volume 2142 of {\em LNCS}, 2001.
240:
241: \bibitem{Reynolds00IntuitionisticReasoningMutable}
242: J.~C. Reynolds.
243: \newblock Intuitionistic reasoning about shared mutable data structure.
244: \newblock In {\em Proceedings of the Symposium in Celebration of the Work of
245: C.A.R. Hoare}, 2000.
246:
247: \bibitem{Reynolds02SeparationLogic}
248: J.~C. Reynolds.
249: \newblock Separation logic: a logic for shared mutable data structures.
250: \newblock In {\em 17th LICS}, pages 55--74, 2002.
251:
252: \bibitem{SagivETAL99Parametric}
253: M.~Sagiv, T.~Reps, and R.~Wilhelm.
254: \newblock Parametric shape analysis via 3-valued logic.
255: \newblock In {\em Proc. 26th ACM POPL}, 1999.
256:
257: \bibitem{SagivETAL02Parametric}
258: M.~Sagiv, T.~Reps, and R.~Wilhelm.
259: \newblock Parametric shape analysis via 3-valued logic.
260: \newblock {\em ACM TOPLAS}, 24(3):217--298, 2002.
261:
262: \bibitem{Skolem19Untersuchungen}
263: T.~Skolem.
264: \newblock Untersuchungen \"uber die {A}xiome des {K}lassenkalk\"uls and \"uber
265: ``{P}roduktations- und {S}ummationsprobleme'', welche gewisse {K}lassen von
266: {A}ussagen betreffen.
267: \newblock Skrifter utgit av {V}idnskapsselskapet i {K}ristiania, I. klasse, no.
268: 3, {O}slo, 1919.
269:
270: \bibitem{SmithETAL00AliasTypes}
271: F.~Smith, D.~Walker, and G.~Morrisett.
272: \newblock Alias types.
273: \newblock In {\em Proc. 9th ESOP}, Berlin, Germany, Mar. 2000.
274:
275: \bibitem{WalkerMorrisett00AliasTypesRecursive}
276: D.~Walker and G.~Morrisett.
277: \newblock Alias types for recursive data structures.
278: \newblock In {\em Workshop on Types in Compilation}, 2000.
279:
280: \bibitem{WilhelmETAL00ShapeAnalysis}
281: R.~Wilhelm, M.~Sagiv, and T.~Reps.
282: \newblock Shape analysis.
283: \newblock In {\em Proc. 9th International Conference on Compiler Construction},
284: Berlin, Germany, 2000. Springer-Verlag.
285:
286: \bibitem{Yahav01VerifyingSafetyPropertiesConcurrentJava}
287: E.~Yahav.
288: \newblock Verifying safety properties of concurrent {J}ava programs using
289: 3-valued logic.
290: \newblock In {\em Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on
291: Principles of programming languages}, pages 27--40. ACM Press, 2001.
292:
293: \bibitem{YahavETAL03VerifyingTemporalHeapPropertiesSpecifiedEvolutionLogic}
294: E.~Yahav, T.~Reps, M.~Sagiv, and R.~Wilhelm.
295: \newblock Verifying temporal heap properties specified via evolution logic.
296: \newblock In {\em Proc. 12th ESOP}, 2003.
297:
298: \end{thebibliography}
299: