Solving quantified first order formulas in Satisfiability Modulo Theories
Yeting Ge · 2010
In writing this dissertation, I have benefited from the support, advice and good will from many people to whom I am eternally grateful. I would like to extend my first thanks to my adviser, Dr. Clark Barrett, for his support, guidance and patience, as well as for his painstakingly editing my dissertation draft to the point of completion. I also want to acknowledge my gratitude toward Dr. Leonardo de Moura for mentoring me at Microsoft Research and working with me on a major part of this dissertation. I would like to thank Dr. Amir Pneuli who over the years had given me great encouragements and had been on my dissertation defense committee. I also would like to express my appreciations to my dissertation defense committee members: Dr. Benjamin Goldberg, Dr. Ernest Davis, and Dr. Morgan Deters. Many thanks to Dr. Morgan Deters for his careful proof reading. I would like to thank other members of the ACSys group for many excellent suggestions on this dissertation.