cs0612003/refs.bbl
1: \newcommand{\etalchar}[1]{$^{#1}$}
2: \begin{thebibliography}{BMMR01}
3: 
4: \bibitem[BCDR04]{ball-tacas04}
5: T.~Ball, B.~Cook, S.~Das, and S.~K. Rajamani.
6: \newblock {Refining Approximations in Software Predicate Abstraction}.
7: \newblock In Kurt Jensen and Andreas Podelski, editors, {\em Proc. Tools and
8:   Algorithms for the Construction and Analysis of Systems (TACAS '04)}, LNCS
9:   2988, pages 388--403. Springer-Verlag, 2004.
10: 
11: \bibitem[BCLZ04]{ball-cav04}
12: T.~Ball, B.~Cook, S.~K. Lahiri, and L.~Zhang.
13: \newblock {Zapato: Automatic Theorem Proving for Software Predicate Abstraction
14:   Refinement}.
15: \newblock In R.~Alur and D.~Peled, editors, {\em Computer Aided Verification
16:   (CAV '04)}, LNCS 3114. Springer-Verlag, 2004.
17: 
18: \bibitem[BMMR01]{ball-pldi01}
19: T.~Ball, R.~Majumdar, T.~Millstein, and S.~K. Rajamani.
20: \newblock Automatic predicate abstraction of {C} programs.
21: \newblock In {\em Programming Language Design and Implementation (PLDI '01)},
22:   pages 203--213, Snowbird, Utah, June, 2001.
23: \newblock {\em SIGPLAN Notices,} 36(5), May 2001.
24: 
25: \bibitem[Bry86]{bryant-tc86}
26: R.~E. Bryant.
27: \newblock Graph-based algorithms for {B}oolean function manipulation.
28: \newblock {\em {IEEE Transactions on Computers}}, C-35(8):677--691, August
29:   1986.
30: 
31: \bibitem[CCG{\etalchar{+}}04]{magic-tse04}
32: S.~Chaki, E.~M. Clarke, A.~Groce, S.~Jha, and H.~Veith.
33: \newblock {Modular Verification of Software Components in C}.
34: \newblock {\em IEEE Transactions on Software Engineering}, 30(6):388--402, June
35:   2004.
36: 
37: \bibitem[CKSY04]{clarke-fmsd04}
38: E.~Clarke, D.~Kroening, N.~Sharygina, and K.~Yorav.
39: \newblock Predicate abstraction of {ANSI--C} programs using {SAT}.
40: \newblock {\em Formal Methods in System Design (FMSD)}, 25:105--127,
41:   September--November 2004.
42: 
43: \bibitem[CLR90]{cormen-book}
44: T.~H. Cormen, C.~E. Leiserson, and R.~L. Rivest.
45: \newblock {\em Introduction to Algorithms}.
46: \newblock MIT Press, 1990.
47: 
48: \bibitem[{CUD}]{cudd-www}
49: {CUDD:CU Decision Diagram Package}.
50: \newblock {\\Available at {\tt
51:   http://vlsi.colorado.edu/\verb|~|fabio/CUDD/cuddIntro.html}}.
52: 
53: \bibitem[DD01]{das-lics01}
54: S.~Das and D.~Dill.
55: \newblock Successive approximation of abstract transition relations.
56: \newblock In {\em {IEEE Symposium of Logic in Computer Science(LICS~'01)}},
57:   pages 51--60. IEEE Computer Society, June 2001.
58: 
59: \bibitem[DDP99]{das-cav99}
60: S.~Das, D.~Dill, and S.~Park.
61: \newblock Experience with predicate abstraction.
62: \newblock In N.~Halbwachs and D.~Peled, editors, {\em {Computer-Aided
63:   Verification (CAV~'99)}}, LNCS 1633, pages 160--171. Springer-Verlag, July
64:   1999.
65: 
66: \bibitem[DE73]{fourier-motzkin}
67: G.B. Dantzig and B.~C. Eaves.
68: \newblock Fourier-motzkin elimination and its dual.
69: \newblock {\em {Journal of Combinatorial Theory}}, A(14):288--297, 1973.
70: 
71: \bibitem[FQ02]{flanagan-popl02}
72: C.~Flanagan and S.~Qadeer.
73: \newblock Predicate abstraction for software verification.
74: \newblock In Launchbury and Mitchell \cite{POPL02}, pages 191--202.
75: 
76: \bibitem[GS97]{graf-cav97}
77: S.~Graf and H.~{Sa\"idi}.
78: \newblock Construction of abstract state graphs with {PVS}.
79: \newblock In O.~Grumberg, editor, {\em {Computer-Aided Verification (CAV
80:   '97)}}, LNCS 1254. Springer-Verlag, June 1997.
81: 
82: \bibitem[HJMS02]{henzinger-popl02}
83: T.~A. Henzinger, R.~Jhala, R.~Majumdar, and G.~Sutre.
84: \newblock {Lazy Abstraction}.
85: \newblock In Launchbury and Mitchell \cite{POPL02}, pages 58--70.
86: 
87: \bibitem[JM05]{jhala-cav05}
88: R.~Jhala and K.~L. McMillan.
89: \newblock Interpolant-based transition relation approximation.
90: \newblock In Kousha Etessami and Sriram~K. Rajamani, editors, {\em Computer
91:   Aided Verification (CAV '05)}, volume 3576 of {\em Lecture Notes in Computer
92:   Science}, pages 39--51. Springer, 2005.
93: 
94: \bibitem[LBC03]{lahiri-cav03a}
95: S.~K. Lahiri, R.~E. Bryant, and B.~Cook.
96: \newblock A symbolic approach to predicate abstraction.
97: \newblock In W.~A. {Hunt, Jr.} and F.~Somenzi, editors, {\em Computer-Aided
98:   Verification (CAV 2003)}, LNCS 2725, pages 141--153. Springer-Verlag, 2003.
99: 
100: \bibitem[LM02]{POPL02}
101: John Launchbury and John~C. Mitchell, editors.
102: \newblock {\em Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on
103:   Principles of programming languages (POPL '02)}. ACM Press, 2002.
104: 
105: \bibitem[McM02]{mcmillan-cav02}
106: K.~McMillan.
107: \newblock {Applying SAT Methods in Unbounded Symbolic Model Checking}.
108: \newblock In E.~Brinksma and K.~G. Larsen, editors, {\em Proc. Computer-Aided
109:   Verification ({CAV}'02)}, LNCS 2404, pages 250--264, July 2002.
110: 
111: \bibitem[NK00]{namjoshi-cav00}
112: K.~S. Namjoshi and R.~P. Kurshan.
113: \newblock Syntactic program transformations for automatic abstraction.
114: \newblock In A.~Emerson and P.~Sistla, editors, {\em Computer Aided
115:   Verification}, LNCS 1855, pages 435--449, 2000.
116: 
117: \bibitem[NO79]{nelson-toplas79}
118: G.~Nelson and D.~C. Oppen.
119: \newblock Simplification by cooperating decision procedures.
120: \newblock {\em {ACM Transactions on Programming Languages and Systems
121:   (TOPLAS)}}, 2(1):245--257, 1979.
122: 
123: \bibitem[NO80]{nelson-jacm80}
124: G.~Nelson and D.~C. Oppen.
125: \newblock Fast decision procedures based on the congruence closure.
126: \newblock {\em {Journal of the ACM}}, 27(2):356--364, 1980.
127: 
128: \bibitem[SS99]{saidi-cav99}
129: H.~{Sa\"idi} and N.~Shankar.
130: \newblock Abstract and model check while you prove.
131: \newblock In N.~Halbwachs and D.~Peled, editors, {\em Computer-Aided
132:   Verification}, volume 1633 of {\em LNCS}, pages 443--454. Springer-Verlag,
133:   July 1999.
134: 
135: \bibitem[SSB02]{strichman-cav02}
136: O.~Strichman, S.~A. Seshia, and R.~E. Bryant.
137: \newblock {Deciding Separation Formulas with SAT}.
138: \newblock In E.~Brinksma and K.~G. Larsen, editors, {\em Proc. Computer-Aided
139:   Verification ({CAV}'02)}, LNCS 2404, pages 209--222, July 2002.
140: 
141: \end{thebibliography}
142: