cs0609104/main.bbl
1: \begin{thebibliography}{10}
2: 
3: \bibitem{BalabanETAL05ShapeAnalysisPredicateAbstraction}
4: I.~Balaban, A.~Pnueli, and L.~Zuck.
5: \newblock Shape analysis by predicate abstraction.
6: \newblock In {\em VMCAI'05}, 2005.
7: 
8: \bibitem{BallETAL01AutomaticPredicateAbstraction}
9: T.~Ball, R.~Majumdar, T.~Millstein, and S.~K. Rajamani.
10: \newblock Automatic predicate abstraction of {C} programs.
11: \newblock In {\em Proc. ACM PLDI}, 2001.
12: 
13: \bibitem{BarrettBerezin04CVCLite}
14: C.~Barrett and S.~Berezin.
15: \newblock {CVC L}ite: A new implementation of the cooperating validity checker.
16: \newblock In R.~Alur and D.~A. Peled, editors, {\em Proceedings of the
17:   $16^{th}$ International Conference on Computer Aided Verification (CAV '04)},
18:   volume 3114 of {\em Lecture Notes in Computer Science}, pages 515--518.
19:   Springer-Verlag, July 2004.
20: \newblock Boston, Massachusetts.
21: 
22: \bibitem{BinghamRakamaric05LogicDecisionProcedure}
23: J.~Bingham and Z.~Rakamari\'c.
24: \newblock A logic and decision procedure for predicate abstraction of
25:   heap-manipulating programs.
26: \newblock Technical Report TR-2005-19, UBC Department of Computer Science,
27:   September 2005.
28: 
29: \bibitem{Bryant86GraphBasedAlgorithmsBooleanFunctionManipulation}
30: R.~E. Bryant.
31: \newblock Graph-based algorithms for boolean function manipulation.
32: \newblock {\em IEEE Transactions on Computers}, C-35(8):677--691, August 1986.
33: 
34: \bibitem{CalvaneseETAL99ReasoningExpressiveDescriptionLogicsFixpoints}
35: D.~Calvanese, G.~De~Giacomo, and M.~Lenzerini.
36: \newblock Reasoning in expressive description logics with fixpoints based on
37:   automata on infinite trees.
38: \newblock In {\em Proc. of the 16th Int. Joint Conf. on Artificial Intelligence
39:   (IJCAI'99)}, pages 84--89, 1999.
40: 
41: \bibitem{CousotCousot77AbstractInterpretation}
42: P.~Cousot and R.~Cousot.
43: \newblock Abstract interpretation: a unified lattice model for static analysis
44:   of programs by construction or approximation of fixpoints.
45: \newblock In {\em Proc. 4th POPL}, 1977.
46: 
47: \bibitem{DistefanoETAL06LocalShapeAnalysisBasedSeparationLogic}
48: D.~Distefano, P.~O'Hearn, and H.~Yang.
49: \newblock A local shape analysis based on separation logic.
50: \newblock In {\em TACAS'06}, 2006.
51: 
52: \bibitem{FlanaganQadeer02PredicateAbstraction}
53: C.~Flanagan and S.~Qadeer.
54: \newblock Predicate abstraction for software verification.
55: \newblock In {\em Proc. 29th ACM POPL}, 2002.
56: 
57: \bibitem{FlanaganSaxe01AvoidingExponentialExplosion}
58: C.~Flanagan and J.~B. Saxe.
59: \newblock Avoiding exponential explosion: {G}enerating compact verification
60:   conditions.
61: \newblock In {\em Proc. 28th ACM POPL}, 2001.
62: 
63: \bibitem{FradetMetayer97ShapeTypes}
64: P.~Fradet and D.~L. M\'etayer.
65: \newblock Shape types.
66: \newblock In {\em Proc. 24th ACM POPL}, 1997.
67: 
68: \bibitem{GeorgievaMaier05DescriptionLogicsForShapeAnalysis}
69: L.~Georgieva and P.~Maier.
70: \newblock Description logics for shape analysis.
71: \newblock In {\em Proc. 3rd SEFM}, pages 321--330, 2005.
72: 
73: \bibitem{GhiyaHendren96TreeOrDag}
74: R.~Ghiya and L.~Hendren.
75: \newblock Is it a tree, a {DAG}, or a cyclic graph?
76: \newblock In {\em Proc. 23rd ACM POPL}, 1996.
77: 
78: \bibitem{GhiyaHendren95ConnectionAnalysis}
79: R.~Ghiya and L.~J. Hendren.
80: \newblock Connection analysis: A practical interprocedural heap analysis for
81:   {C}.
82: \newblock In {\em Proc. 8th Workshop on Languages and Compilers for Parallel
83:   Computing}, 1995.
84: 
85: \bibitem{Graedel99DecisionProceduresGuardedLogics}
86: E.~Gr{\"a}del.
87: \newblock Decision procedures for guarded logics.
88: \newblock In {\em Automated Deduction - CADE16. Proceedings of 16th
89:   International Conference on Automated Deduction, Trento, 1999}, volume 1632
90:   of {\em {LNCS}}. Springer-Verlag, 1999.
91: 
92: \bibitem{GrafSaidi97ConstructionAbstractStateGraphsPVS}
93: S.~Graf and H.~Saidi.
94: \newblock Construction of abstract state graphs with pvs.
95: \newblock In {\em Proc. 9th CAV}, pages 72--83, 1997.
96: 
97: \bibitem{HenzingerETAL02LazyAbstraction}
98: T.~A. Henzinger, R.~Jhala, R.~Majumdar, and G.~Sutre.
99: \newblock Lazy abstraction.
100: \newblock In {\em POPL}, 2002.
101: 
102: \bibitem{MuchnikJones81ProgramFlowAnalysis}
103: N.~D. Jones and S.~S. Muchnik.
104: \newblock {\em Program Flow Analysis: Theory and Applications}, chapter Chapter
105:   4: Flow Analysis and Optimization of {LISP}-like Structures.
106: \newblock Prentice Hall, 1981.
107: 
108: \bibitem{KlarlundETAL00MONA}
109: N.~Klarlund, A.~M{\o}ller, and M.~I. Schwartzbach.
110: \newblock {MONA} implementation secrets.
111: \newblock In {\em Proc. 5th International Conference on Implementation and
112:   Application of Automata}. LNCS, 2000.
113: 
114: \bibitem{KlarlundSchwartzbach93GraphTypes}
115: N.~Klarlund and M.~I. Schwartzbach.
116: \newblock Graph types.
117: \newblock In {\em Proc. 20th ACM POPL}, Charleston, SC, 1993.
118: 
119: \bibitem{Kuncak06JahobProjectWebPage}
120: V.~Kuncak.
121: \newblock The {J}ahob project web page.
122: \newblock http://www.mit.edu/$\sim$vkuncak/projects/jahob/, 2006.
123: 
124: \bibitem{KuncakETAL06ProposalEstablishShapeAnalysisBenchmarks}
125: V.~Kuncak, S.~Lahiri, R.~Rugina, E.~Yahav, and T.~Wies.
126: \newblock A proposal to establish shape analysis benchmarks.
127: \newblock POPL 2006, Charleston, South Carolina, January 2006.
128: 
129: \bibitem{KuncakETAL02RoleAnalysis}
130: V.~Kuncak, P.~Lam, and M.~Rinard.
131: \newblock Role analysis.
132: \newblock In {\em Annual ACM Symp.\ on Principles of Programming Languages
133:   (POPL)}, 2002.
134: 
135: \bibitem{LahiriBryant04IndexedPredicateDiscoveryUnboundedSystemVerification}
136: S.~K. Lahiri and R.~E. Bryant.
137: \newblock Indexed predicate discovery for unbounded system verification.
138: \newblock In {\em CAV'04}, 2004.
139: 
140: \bibitem{LahiriQadeer06VerifyingPropertiesWellFoundedLinkedLists}
141: S.~K. Lahiri and S.~Qadeer.
142: \newblock Verifying properties of well-founded linked lists.
143: \newblock In {\em POPL'06}, 2006.
144: 
145: \bibitem{LamETAL05HobTool}
146: P.~Lam, V.~Kuncak, and M.~Rinard.
147: \newblock Hob: A tool for verifying data structure consistency.
148: \newblock In {\em 14th International Conference on Compiler Construction (tool
149:   demo)}, April 2005.
150: 
151: \bibitem{LamETAL04HobProjectWebPage}
152: P.~Lam, V.~Kuncak, K.~Zee, and M.~Rinard.
153: \newblock The {H}ob project web page.
154: \newblock http://hob.csail.mit.edu, 2004.
155: 
156: \bibitem{LeeETAL05AutomaticVerificationPointerProgramsUsing}
157: O.~Lee, H.~Yang, and K.~Yi.
158: \newblock Automatic verification of pointer programs using grammar-based shape
159:   analysis.
160: \newblock In {\em ESOP}, 2005.
161: 
162: \bibitem{LevAmiETAL05SimulatingReachabilityFirstOrderLogic}
163: T.~Lev-Ami, N.~Immerman, T.~Reps, M.~Sagiv, S.~Srivastava, and G.~Yorsh.
164: \newblock Simulating reachability using first-order logic with applications to
165:   verification of linked data structures.
166: \newblock In {\em CADE-20}, 2005.
167: 
168: \bibitem{LevAmiETAL00PuttingStaticAnalysisWorkVerification}
169: T.~Lev-Ami, T.~Reps, M.~Sagiv, and R.~Wilhelm.
170: \newblock Putting static analysis to work for verification: A case study.
171: \newblock In {\em International Symposium on Software Testing and Analysis},
172:   2000.
173: 
174: \bibitem{ManevichETAL05PredicateAbstractionCanonicalAbstractionSinglyLinkedLis%
175: ts}
176: R.~Manevich, E.~Yahav, G.~Ramalingam, and M.~Sagiv.
177: \newblock Predicate abstraction and canonical abstraction for singly-linked
178:   lists.
179: \newblock In {\em 6th VMCAI}, pages 181--198, 2005.
180: 
181: \bibitem{Moeller01PALE}
182: A.~M{\o}ller and M.~I. Schwartzbach.
183: \newblock The {P}ointer {A}ssertion {L}ogic {E}ngine.
184: \newblock In {\em Programming Language Design and Implementation}, 2001.
185: 
186: \bibitem{Nelson83VerifyingReachabilityInvariantsLinkedStructures}
187: G.~Nelson.
188: \newblock Verifying reachability invariants of linked structures.
189: \newblock In {\em POPL}, 1983.
190: 
191: \bibitem{NipkowETAL02IsabelleHOL}
192: T.~Nipkow, L.~C. Paulson, and M.~Wenzel.
193: \newblock {\em Isabelle/HOL: A Proof Assistant for Higher-Order Logic}, volume
194:   2283 of {\em LNCS}.
195: \newblock Springer-Verlag, 2002.
196: 
197: \bibitem{PodelskiWies05BooleanHeaps}
198: A.~Podelski and T.~Wies.
199: \newblock Boolean heaps.
200: \newblock In {\em Proc.\ Int.\ Static Analysis Symposium}, 2005.
201: 
202: \bibitem{RaniseZarba05DecidableLogicPointerProgramsManipulatingLinkedLists}
203: S.~Ranise and C.~G. Zarba.
204: \newblock A decidable logic for pointer programs manipulating linked lists,
205:   2005.
206: 
207: \bibitem{Reineke05ShapeAnalysisSets}
208: J.~Reineke.
209: \newblock Shape analysis of sets.
210: \newblock Master's thesis, Universit\"at des Saarlandes, Germany, June 2005.
211: 
212: \bibitem{RepsETAL03FiniteDifferencingLogicalFormulasStaticAnalysis}
213: T.~Reps, M.~Sagiv, and A.~Loginov.
214: \newblock Finite differencing of logical formulas for static analysis.
215: \newblock In {\em Proc. 12th ESOP}, 2003.
216: 
217: \bibitem{SagivETAL02Parametric}
218: M.~Sagiv, T.~Reps, and R.~Wilhelm.
219: \newblock Parametric shape analysis via 3-valued logic.
220: \newblock {\em ACM TOPLAS}, 24(3):217--298, 2002.
221: 
222: \bibitem{Voronkov95Vampire}
223: A.~Voronkov.
224: \newblock The anatomy of {V}ampire (implementing bottom-up procedures with code
225:   trees).
226: \newblock {\em Journal of Automated Reasoning}, 15(2):237--265, 1995.
227: 
228: \bibitem{Spass}
229: C.~Weidenbach.
230: \newblock Combining superposition, sorts and splitting.
231: \newblock In A.~Robinson and A.~Voronkov, editors, {\em Handbook of Automated
232:   Reasoning}, volume~II, chapter~27, pages 1965--2013. Elsevier Science, 2001.
233: 
234: \bibitem{Wies04SymbolicShapeAnalysis}
235: T.~Wies.
236: \newblock Symbolic shape analysis.
237: \newblock Master's thesis, Universit\"at des Saarlandes, Saarbr\"ucken,
238:   Germany, September 2004.
239: 
240: \bibitem{WiesETAL06FieldConstraintAnalysis}
241: T.~Wies, V.~Kuncak, P.~Lam, A.~Podelski, and M.~Rinard.
242: \newblock Field constraint analysis.
243: \newblock In {\em Proc.\ Int.\ Conf.\ Verification, Model Checking, and
244:   Abstract Interpratation}, 2006.
245: 
246: \bibitem{YorshETAL06LogicReachablePatternsLinkedDataStructures}
247: G.~Yorsh, A.~Rabinovich, M.~Sagiv, A.~Meyer, and A.~Bouajjani.
248: \newblock A logic of reachable patterns in linked data-structures.
249: \newblock In {\em Proc. Foundations of Software Science and Computation
250:   Structures (FOSSACS 2006)}, 2006.
251: 
252: \bibitem{YorshETAL04SymbolicallyComputingMostPrecise}
253: G.~Yorsh, T.~Reps, and M.~Sagiv.
254: \newblock Symbolically computing most-precise abstract operations for shape
255:   analysis.
256: \newblock In {\em 10th TACAS}, 2004.
257: 
258: \bibitem{YorshETAL05LogicalCharacterizationsHeapAbstractions}
259: G.~Yorsh, T.~Reps, M.~Sagiv, and R.~Wilhelm.
260: \newblock Logical characterizations of heap abstractions.
261: \newblock {\em TOCL}, 2005.
262: \newblock (to appear).
263: 
264: \bibitem{YorshETAL05AutomaticAssumeGuaranteeReasoningHeap}
265: G.~Yorsh, A.~Skidanov, T.~Reps, and M.~Sagiv.
266: \newblock Automatic assume/guarantee reasoning for heap-manupilating programs.
267: \newblock In {\em 1st AIOOL Workshop}, 2005.
268: 
269: \bibitem{ZeeETAL04CombiningTheoremStaticAnalysisDataStructureConsistency}
270: K.~Zee, P.~Lam, V.~Kuncak, and M.~Rinard.
271: \newblock Combining theorem proving with static analysis for data structure
272:   consistency.
273: \newblock In {\em International Workshop on Software Verification and
274:   Validation (SVV 2004)}, Seattle, November 2004.
275: 
276: \end{thebibliography}
277: