cs0408014/main.bbl
1: \begin{thebibliography}{10}
2: 
3: \bibitem{BoergerETAL97ClassicalDecisionProblem}
4: Egon B\"orger, Erich Gr\"aedel, and Yuri Gurevich.
5: \newblock {\em The Classical Decision Problem}.
6: \newblock Springer-Verlag, 1997.
7: 
8: \bibitem{ChaseETAL90AnalysisPointersStructures}
9: David~R. Chase, Mark Wegman, and F.~Kenneth Zadeck.
10: \newblock Analysis of pointers and structures.
11: \newblock In {\em Proc. ACM PLDI}, 1990.
12: 
13: \bibitem{ComonETAL97Tata}
14: H.~Comon, M.~Dauchet, R.~Gilleron, F.~Jacquemard, D.~Lugiez, S.~Tison, and
15:   M.~Tommasi.
16: \newblock Tree automata techniques and applications.
17: \newblock Available on: {\tt http://www.grappa.univ-lille3.fr/tata}, 1997.
18: \newblock release 1999.
19: 
20: \bibitem{Courcelle97MSOL}
21: Bruno Courcelle.
22: \newblock The expression of graph properties and graph transformations in
23:   monadic second-order logic.
24: \newblock In {\em Handbook of graph grammars and computing by graph
25:   transformations, Vol. 1 : Foundations}, chapter~5. World Scientific, 1997.
26: 
27: \bibitem{DeLineFahndrich01EnforcingHighLevelProtocols}
28: Robert DeLine and Manuel F\"ahndrich.
29: \newblock Enforcing high-level protocols in low-level software.
30: \newblock In {\em Proc. ACM PLDI}, 2001.
31: 
32: \bibitem{DrossopoulouETAL01Reclassification}
33: S.~Drossopoulou, F.~Damiani, M.~Dezani-Ciancaglini, and P.~Giannini.
34: \newblock Fickle: Dynamic object re-classification.
35: \newblock In {\em Proc. 15th European Conference on Object-Oriented
36:   Programming}, LNCS 2072, pages 130--149. Springer, 2001.
37: 
38: \bibitem{FaginETAL95MonadicNPMonadicCoNP}
39: Ronald Fagin, Larry~J. Stockmeyer, and Moshe~Y. Vardi.
40: \newblock On monadic {NP} vs monadic co-{NP}.
41: \newblock {\em Information and Computation}, 120(1), 1995.
42: 
43: \bibitem{FlanaganETAL02ExtendedStaticCheckingJava}
44: Cormac Flanagan, K.~Rustan~M. Leino, Mark Lilibridge, Greg Nelson, James~B.
45:   Saxe, and Raymie Stata.
46: \newblock {E}xtended {S}tatic {C}hecking for {J}ava.
47: \newblock In {\em Proc. ACM PLDI}, 2002.
48: 
49: \bibitem{FradetMetayer97ShapeTypes}
50: Pascal Fradet and Daniel~Le Metayer.
51: \newblock Shape types.
52: \newblock In {\em Proc. 24th ACM POPL}, 1997.
53: 
54: \bibitem{GecsegSteinby97TreeLanguages}
55: Ferenc Gecseg and Magnus Steinby.
56: \newblock Tree languages.
57: \newblock In G.~Rozenberg and A.~Salomaa, editors, {\em Handbook of Formal
58:   Languages. Vol.\ {III}: Beyond Words}, chapter~1. Springer, 1997.
59: 
60: \bibitem{GhiyaHendren96TreeOrDag}
61: Rakesh Ghiya and Laurie Hendren.
62: \newblock Is it a tree, a {DAG}, or a cyclic graph?
63: \newblock In {\em Proc. 23rd ACM POPL}, 1996.
64: 
65: \bibitem{GiammarresiRestivo97TwoDimensionalLanguages}
66: Dora Giammarresi and Antonio Restivo.
67: \newblock Two-dimensional languages.
68: \newblock In Grzegorz Rozenberg and Arto Salomaa, editors, {\em Handbook of
69:   Formal Languages Vol.3: Beyond Words}. Springer-Verlag, 1997.
70: 
71: \bibitem{Kuncak01DesigningRoleAnalysis}
72: Viktor Kuncak.
73: \newblock Designing an algorithm for role analysis.
74: \newblock Master's thesis, MIT Laboratory for Computer Science, 2001.
75: 
76: \bibitem{KuncakETAL02RoleAnalysis}
77: Viktor Kuncak, Patrick Lam, and Martin Rinard.
78: \newblock Role analysis.
79: \newblock In {\em Proc. 29th ACM POPL}, 2002.
80: 
81: \bibitem{KuncakRinard02ReasoningHeapHOL}
82: Viktor Kuncak and Martin Rinard.
83: \newblock Reasoning about the heap in higher order logic.
84: \newblock Technical report, MIT Laboratory for Computer Science, 2002.
85: 
86: \bibitem{LarusHilfinger88DetectingConflictsAccesses}
87: James~R. Larus and Paul~N. Hilfinger.
88: \newblock Detecting conflicts between structure accesses.
89: \newblock In {\em Proc. ACM PLDI}, Atlanta, GA, June 1988.
90: 
91: \bibitem{LeinoStata97CheckingObjectInvariants}
92: K.~Rustan~M. Leino and Raymie Stata.
93: \newblock Checking object invariants.
94: \newblock Technical report, COMPAQ Systems Research Center, 1997.
95: 
96: \bibitem{Moeller01PALE}
97: Anders M{\o}ller and Michael~I. Schwartzbach.
98: \newblock The {P}ointer {A}ssertion {L}ogic {E}ngine.
99: \newblock In {\em Proc. ACM PLDI}, 2001.
100: 
101: \bibitem{SagivETAL96Destructive}
102: Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
103: \newblock Solving shape-analysis problems in languages with destructive
104:   updating.
105: \newblock In {\em Proc. 23rd ACM POPL}, 1996.
106: 
107: \bibitem{SagivETAL99Parametric}
108: Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
109: \newblock Parametric shape analysis via 3-valued logic.
110: \newblock In {\em Proc. 26th ACM POPL}, 1999.
111: 
112: \bibitem{SchwentickBarthelmann01LocalNormalForms}
113: Thomas Schwentick and Klaus Barthelmann.
114: \newblock Local normal forms for first-order logic with applications to games
115:   and automata.
116: \newblock {\em Discrete Mathematics and Theoretical Computer Science}, 2001.
117: 
118: \bibitem{Sipser97TheoryComputation}
119: Michael Sipser.
120: \newblock {\em Introduction to the Theory of Computation}.
121: \newblock PWS Publishing Company, 1997.
122: 
123: \bibitem{SmithETAL00AliasTypes}
124: F.~Smith, D.~Walker, and G.~Morrisett.
125: \newblock Alias types.
126: \newblock In {\em Proc. 9th European Symposium on Programming}, Berlin,
127:   Germany, March 2000.
128: 
129: \bibitem{StromYellin93ExtendingTypestate}
130: Robert~E. Strom and Daniel~M. Yellin.
131: \newblock Extending typestate checking using conditional liveness analysis.
132: \newblock {\em IEEE Transactions on Software Engineering}, May 1993.
133: 
134: \bibitem{StromYemini86Typestate}
135: Robert~E. Strom and Shaula Yemini.
136: \newblock Typestate: A programming language concept for enhancing software
137:   reliability.
138: \newblock {\em IEEE Transactions on Software Engineering}, January 1986.
139: 
140: \bibitem{Thomas91LogicsTilingsAutomata}
141: Wolfgang Thomas.
142: \newblock On logics, tilings, and automata.
143: \newblock In {\em Proc. 18th International Colloquium on Automata, Languages
144:   and Programming}, volume 510 of {\em Lecture Notes in Computer Science},
145:   1991.
146: 
147: \bibitem{Thomas97LanguagesAutomataLogic}
148: Wolfgang Thomas.
149: \newblock Languages, automata, and logic.
150: \newblock In {\em Handbook of Formal Languages Vol.3: Beyond Words}.
151:   Springer-Verlag, 1997.
152: 
153: \bibitem{WalkerMorrisett00AliasTypesRecursive}
154: David Walker and Greg Morrisett.
155: \newblock Alias types for recursive data structures.
156: \newblock In {\em Workshop on Types in Compilation}, 2000.
157: 
158: \end{thebibliography}
159: