1: \begin{thebibliography}{10}
2:
3: \bibitem{Aiken99SetConstraintsIntro}
4: A.~Aiken.
5: \newblock Introduction to set constraint-based program analysis.
6: \newblock {\em Science of Computer Programming}, 35:79--111, 1999.
7:
8: \bibitem{AikenETAL93ComplexitySetConstraints}
9: A.~Aiken, D.~Kozen, M.~Vardi, and E.~Wimmers.
10: \newblock The complexity of set constraints.
11: \newblock In {\em Proceedings of Computer Science Logic 1993}, pages 1--17,
12: September 1993.
13:
14: \bibitem{AikenETAL95DecidabilitySetConstraints}
15: A.~Aiken, D.~Kozen, and E.~Wimmers.
16: \newblock Decidability of systems of set constraints with negative constraints.
17: \newblock {\em Information and Computation}, 122, 1995.
18:
19: \bibitem{AikenWimmers93ConstraintsTypeInference}
20: A.~Aiken and E.~L. Wimmers.
21: \newblock Type inclusion constraints and type inference.
22: \newblock In {\em Proc. 7th ACM Conference on Functional Programming and
23: Computer Architecture}, Copenhagen, Denmark, 1993.
24:
25: \bibitem{BaaderETAL03DescriptionLogicHandbook}
26: F.~Baader, D.~Calvanese, D.~McGuinness, D.~Nardi, and P.~Patel-Schneider,
27: editors.
28: \newblock {\em The Description Logic Handbook: Theory, Implementation and
29: Applications}.
30: \newblock CUP, 2003.
31:
32: \bibitem{BachmairETAL93SetConstraintsMonadicClass}
33: L.~Bachmair, H.~Ganzinger, and U.~Waldmann.
34: \newblock Set constraints are the monadic class.
35: \newblock In {\em Logic in Computer Science}, pages 75--83, 1993.
36:
37: \bibitem{BoergerETAL97ClassicalDecisionProblem}
38: E.~B\"orger, E.~Gr\"adel, and Y.~Gurevich.
39: \newblock {\em The Classical Decision Problem}.
40: \newblock Springer-Verlag, 1997.
41:
42: \bibitem{Bryant86GraphBasedAlgorithmsBooleanFunctionManipulation}
43: R.~E. Bryant.
44: \newblock Graph-based algorithms for boolean function manipulation.
45: \newblock {\em IEEE Transactions on Computers}, C-35(8):677--691, August 1986.
46:
47: \bibitem{CadoliETAL02AlgorithmEvaluateQuantifiedBooleanFormulae}
48: M.~Cadoli, M.~Schaerf, A.~Giovanardi, and M.~Giovanardi.
49: \newblock An algorithm to evaluate quantified boolean formulae and its
50: experimental evaluation.
51: \newblock {\em J. Autom. Reasoning}, 28(2):101--142, 2002.
52:
53: \bibitem{CantoneETAL01SetTheoryComputing}
54: D.~Cantone, E.~Omodeo, and A.~Policriti.
55: \newblock {\em Set Theory for Computing}.
56: \newblock Springer, 2001.
57:
58: \bibitem{Chen76EntityRelationshipModel}
59: P.~P.-S. Chen.
60: \newblock The entity-relationship model--toward a unified view of data.
61: \newblock {\em ACM Transactions on Database Systems (TODS)}, 1(1):9--36, 1976.
62:
63: \bibitem{ComonETAL97Tata}
64: H.~Comon, M.~Dauchet, R.~Gilleron, F.~Jacquemard, D.~Lugiez, S.~Tison, and
65: M.~Tommasi.
66: \newblock Tree automata techniques and applications.
67: \newblock Available on: {\tt http://www.grappa.univ-lille3.fr/tata}, 1997.
68: \newblock release 1999.
69:
70: \bibitem{FaehndrichETAL98PartialOnlineCycleEliminationInclusionConstraintGraph%
71: s}
72: M.~F{\"a}hndrich, J.~Foster, Z.~Su, and A.~Aiken.
73: \newblock Partial online cycle elimination in inclusion constraint graphs.
74: \newblock In {\em PLDI'98}, 1998.
75:
76: \bibitem{FefermanVaught59FirstOrderPropertiesProductsAlgebraicSystems}
77: S.~Feferman and R.~L. Vaught.
78: \newblock The first order properties of products of algebraic systems.
79: \newblock {\em Fundamenta Mathematicae}, 47:57--103, 1959.
80:
81: \bibitem{FisherRabin74SuperExponentialComplexityPresburgerArithmetic}
82: M.~J. Fisher and M.~O. Rabin.
83: \newblock Super-exponential complexity of presburger arithmetic.
84: \newblock {\em SIAM-AMS Proceedings}, 7, 1974.
85:
86: \bibitem{FlanaganETAL03TheoremProvingUsingLazyProofExplication}
87: C.~Flanagan, R.~Joshi, X.~Ou, and J.~B. Saxe.
88: \newblock Theorem proving using lazy proof explication.
89: \newblock In {\em CAV}, pages 355--367, 2003.
90:
91: \bibitem{GanzingerETAL04DPLLT}
92: H.~Ganzinger, G.~Hagen, R.~Nieuwenhuis, A.~Oliveras, and C.~Tinelli.
93: \newblock {DPLL(T)}: Fast decision procedures.
94: \newblock In R.~Alur and D.~Peled, editors, {\em 16th CAV}, volume 3114 of {\em
95: LNCS}, pages 175--188. Springer, 2004.
96:
97: \bibitem{GivanETAL02TarskianSetConstraints}
98: R.~Givan, D.~McAllester, C.~Witty, and D.~Kozen.
99: \newblock Tarskian set constraints.
100: \newblock {\em Inf. Comput.}, 174(2):105--131, 2002.
101:
102: \bibitem{GraedelETAL97TwoVariableLogicCountingDecidable}
103: E.~Gr{\"a}del, M.~Otto, and E.~Rosen.
104: \newblock Two-variable logic with counting is decidable.
105: \newblock In {\em Proceedings of 12th IEEE Symposium on Logic in Computer
106: Science LICS `97, Warschau}, 1997.
107:
108: \bibitem{KodumalAiken04SetConstraintCFLReachabilityConnection}
109: J.~Kodumal and A.~Aiken.
110: \newblock The set constraint/{CFL} reachability connection in practice.
111: \newblock In {\em Proc. ACM PLDI}, June 2004.
112:
113: \bibitem{Kozen80ComplexityBooleanAlgebras}
114: D.~Kozen.
115: \newblock Complexity of boolean algebras.
116: \newblock {\em Theoretical Computer Science}, 10:221--247, 1980.
117:
118: \bibitem{KuncakETAL05AlgorithmDecidingBAPA}
119: V.~Kuncak, H.~H. Nguyen, and M.~Rinard.
120: \newblock An algorithm for deciding {BAPA}: {B}oolean {A}lgebra with
121: {P}resburger {A}rithmetic.
122: \newblock In {\em 20th International Conference on Automated Deduction,
123: CADE-20}, Tallinn, Estonia, July 2005.
124:
125: \bibitem{KuncakRinard04FirstOrderTheorySetsCardinalityConstraintsDecidable}
126: V.~Kuncak and M.~Rinard.
127: \newblock The first-order theory of sets with cardinality constraints is
128: decidable.
129: \newblock Technical Report 958, MIT CSAIL, July 2004.
130:
131: \bibitem{KuncakRinard04DecisionProcedureSetValuedFields}
132: V.~Kuncak and M.~Rinard.
133: \newblock On decision procedures for set-valued fields.
134: \newblock Technical Report 975, MIT CSAIL, November 2004.
135:
136: \bibitem{KuncakRinard05DecisionProceduresSetValuedFields}
137: V.~Kuncak and M.~Rinard.
138: \newblock Decision procedures for set-valued fields.
139: \newblock In {\em 1st International Workshop on Abstract Interpretation of
140: Object-Oriented Languages (AIOOL 2005)}, 2005.
141:
142: \bibitem{LamETAL04GeneralizedTypestateCheckingUsingSets}
143: P.~Lam, V.~Kuncak, and M.~Rinard.
144: \newblock Generalized typestate checking using set interfaces and pluggable
145: analyses.
146: \newblock {\em SIGPLAN Notices}, 39:46--55, March 2004.
147:
148: \bibitem{LamETAL04OurExperienceModularPluggableAnalyses}
149: P.~Lam, V.~Kuncak, and M.~Rinard.
150: \newblock On our experience with modular pluggable analyses.
151: \newblock Technical Report 965, MIT CSAIL, September 2004.
152:
153: \bibitem{LamETAL05CrossCuttingTechniquesProgramSpecificationAnalysis}
154: P.~Lam, V.~Kuncak, and M.~Rinard.
155: \newblock Cross-cutting techniques in program specification and analysis.
156: \newblock In {\em 4th International Conference on Aspect-Oriented Software
157: Development (AOSD'05)}, 2005.
158:
159: \bibitem{LamETAL05GeneralizedTypestateCheckingDataStructureConsistency}
160: P.~Lam, V.~Kuncak, and M.~Rinard.
161: \newblock Generalized typestate checking for data structure consistency.
162: \newblock In {\em 6th International Conference on Verification, Model Checking
163: and Abstract Interpretation}, 2005.
164:
165: \bibitem{LamETAL05HobTool}
166: P.~Lam, V.~Kuncak, and M.~Rinard.
167: \newblock Hob: A tool for verifying data structure consistency.
168: \newblock In {\em 14th International Conference on Compiler Construction (tool
169: demo)}, April 2005.
170:
171: \bibitem{Loewenheim15UeberMoegligkeitenRelativkalkuel}
172: L.~Loewenheim.
173: \newblock {\"{U}ber} m\"ogligkeiten im relativkalk\"ul.
174: \newblock {\em Math. Annalen}, 76:228--251, 1915.
175:
176: \bibitem{MarnetteETAL05AlgorithmsComplexitySetsCardinalityConstraints}
177: B.~Marnette, V.~Kuncak, and M.~Rinard.
178: \newblock On algorithms and complexity for sets with cardinality constraints.
179: \newblock Technical report, MIT CSAIL, August 2005.
180:
181: \bibitem{MarriottOdersky94NegativeBooleanConstraints}
182: K.~Marriott and M.~Odersky.
183: \newblock Negative boolean constraints.
184: \newblock Technical Report 94/203, Monash University, August 1994.
185:
186: \bibitem{MelskiReps00InterconvertibilitySetConstraintsCFLReachability}
187: D.~Melski and T.~Reps.
188: \newblock Interconvertibility of a class of set constraints and context-free
189: language reachability.
190: \newblock {\em TCS}, 248:29--98, November 2000.
191:
192: \bibitem{PacholskiETAL00ComplexityResultsFirstOrderTwo}
193: L.~Pacholski, W.~Szwast, and L.~Tendera.
194: \newblock Complexity results for first-order two-variable logic with counting.
195: \newblock {\em SIAM J. on Computing}, 29(4):1083--1117, 2000.
196:
197: \bibitem{Papadimitriou81ComplexityIntegerProgramming}
198: C.~H. Papadimitriou.
199: \newblock On the complexity of integer programming.
200: \newblock {\em J. ACM}, 28(4):765--768, 1981.
201:
202: \bibitem{PlaistedETAL03SatisfiabilityProcedureQuantifiedBooleanFormulae}
203: D.~A. Plaisted, A.~Biere, and Y.~Zhu.
204: \newblock A satisfiability procedure for quantified boolean formulae.
205: \newblock {\em Discrete Appl. Math.}, 130(2):291--328, 2003.
206:
207: \bibitem{PrattHartmann04CountingQuantifiersStellarFragment}
208: I.~Pratt-Hartmann.
209: \newblock Counting quantifiers and the stellar fragment.
210: \newblock http://www.cs.man.ac.uk/\~{}ipratt/papers/logic/f2.ps, 2004.
211:
212: \bibitem{Revesz04QuantifierEliminationFirstOrderTheory}
213: P.~Revesz.
214: \newblock Quantifier-elimination for the first-order theory of boolean algebras
215: with linear cardinality constraints.
216: \newblock In {\em Proc. Advances in Databases and Information Systems
217: (ADBIS'04)}, volume 3255 of {\em LNCS}, September 2004.
218:
219: \bibitem{RumbaughETAL99UMLReference}
220: J.~Rumbaugh, I.~Jacobson, and G.~Booch.
221: \newblock {\em The Unified Modelling Language Reference Manual}.
222: \newblock Addison-Wesley, Reading, Mass., 1999.
223:
224: \bibitem{Sipser97TheoryComputation}
225: M.~Sipser.
226: \newblock {\em Introduction to the Theory of Computation}.
227: \newblock PWS Publishing Company, 1997.
228:
229: \bibitem{Skolem19Untersuchungen}
230: T.~Skolem.
231: \newblock Untersuchungen \"uber die {A}xiome des {K}lassenkalk\"uls and \"uber
232: ``{P}roduktations- und {S}ummationsprobleme'', welche gewisse {K}lassen von
233: {A}ussagen betreffen.
234: \newblock Skrifter utgit av {V}idnskapsselskapet i {K}ristiania, I. klasse, no.
235: 3, {O}slo, 1919.
236:
237: \bibitem{Tarski49ArithmeticalClassesTypesBooleanAlgebras}
238: A.~Tarski.
239: \newblock Arithmetical classes and types of boolean algebras.
240: \newblock {\em Bull.\ Amer.\ Math.\ Soc.}, 55, 64, 1192, 1949.
241:
242: \bibitem{Zarba04QuantifierEliminationAlgorithmSetCardinality}
243: C.~G. Zarba.
244: \newblock A quantifier elimination algorithm for a fragment of set theory
245: involving the cardinality operator.
246: \newblock In {\em 18th International Workshop on Unification}, 2004.
247:
248: \bibitem{Zarba05CombiningSetsCardinals}
249: C.~G. Zarba.
250: \newblock Combining sets with cardinals.
251: \newblock {\em Journal of Automated Reasoning}, 34(1), 2005.
252:
253: \bibitem{ZeeETAL04CombiningTheoremStaticAnalysisDataStructureConsistency}
254: K.~Zee, P.~Lam, V.~Kuncak, and M.~Rinard.
255: \newblock Combining theorem proving with static analysis for data structure
256: consistency.
257: \newblock In {\em International Workshop on Software Verification and
258: Validation (SVV 2004)}, Seattle, November 2004.
259:
260: \bibitem{ZhangETAL01EfficientConflictDrivenLearningBooleanSatisfiabilitySolver}
261: L.~Zhang, C.~F. Madigan, M.~W. Moskewicz, and S.~Malik.
262: \newblock Efficient conflict driven learning in boolean satisfiability solver.
263: \newblock In {\em ICCAD}, pages 279--285, 2001.
264:
265: \bibitem{ZhangMalik02ConflictBooleanSatisfiability}
266: L.~Zhang and S.~Malik.
267: \newblock Conflict driven learning in a quantified boolean satisfiability
268: solver.
269: \newblock In {\em ICCAD '02: Proceedings of the 2002 IEEE/ACM international
270: conference on Computer-aided design}, pages 442--449, New York, NY, USA,
271: 2002. ACM Press.
272:
273: \end{thebibliography}
274: