Timothy Murphy will present his General Exam on Tuesday January 23, 2018 at 12pm in CS 401. The members of his committee are as follows: Zak Kincaid (Advisor), Aarti Gupta, and David Walker. Please find his reading list and abstract below. Papers / Chapters: 1. "Well Structured Transition Systems Everywhere." A Finkel and Ph. Schnoebelen. 1999. 2. "An axiomatic Proof Technique for Parallel Programs I." Susan Owici and David Gries. 1976. 3. "Resources, Concurrency and Local Reasoning." Peter W O'Hearn. 2004. 4. "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints." Patric Cousot and Radhia Cousot. 1977. 5. "Lazy Abstraction with Interpolants." K. L. McMillan. 2006. 6. "Proof Spaces for Unbounded Parallelism." Azadeh Farzan, Zak Kincaid, and Andreas Podelski. 2015. 7. "The rely-Gaurantee Method for Verifying Shared Variable Programs." Qiwen Xu, Willem-Paul de Rolver and Jifeng He. 1997. 8. "A filtering Algorithm for Constraints of difference in CSPs." Jean-Charles Regin. 1996. 9. "Synethesizing Software Verifies from Proof Rules." Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. 2012. 10. "Artificial Intelligence: A Modern Approach" Chapter 6. (CSPs). Peter Norvig and Stuart J. Russel. 1994. Textbooks: 1. "The Calculus of Computation." Bradley and Manna. 2. "Principles of Program Analysis." Nielson, Nielson, and Hankin Abstract: I will start by introducing the concept of Predicate Automata and their use in concurrent program verification. Next, I'll describe the challenge of emptiness checking for such Predicate Automata --- How does one determine when to stop expanding a configuration of states? To do this, I introduce the notion of covering. If a configuration is covered by another already expanded configuration, then we can safely stop expanding. I will then show that the problem of determining coverability between two configurations is equivalent to the structure embedding problem. Finally, I’ll present MatchEmbeds, an algorithm for the structure embedding problem: given two finite first-order structures over a common relational vocabulary, does there exist an injective homomorphism from one to the other? The structure embedding problem is NP-complete in the general case, but for monadic structures (each predicate has arity 1) I observe that it can be solved in polytime by reduction to bipartite graph matching. My algorithm extends the bipartite matching approach to the general case by using it as the foundation of a backtracking search procedure. I show that MatchEmbeds outperforms state-of-the-art constraint satisfaction solvers on difficult random instances and significantly improves the performance of a client model checker for multi-threaded programs.