Acknowledgements

I would like to thank my advisor Clark Barrett. Without his support, this the-sis would not have been possible. I would also like to thank the other members of my reading committee: Thomas Wies and Margaret Wright. Throughout this process, I have been exceptionally fortunate to have been guided and advised by a large number of talented researchers, including David Dill, Bruno Dutertre