Jake Silverman will present his General Exam on May 7, 2019 at 2pm in CS 302. The members of his committee are as follows: Zak Kincaid (adviser), Aarti Gupta, and Andrew Appel. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. Title: Loop Summarization with Rational Vector Addition Systems Abstract: Modern software verification techniques employ a number of heuristics for reasoning about loops. While these heuristics are often effective, they are unpredictable. For example, abstract interpretation analyses sometimes have an unobtainable least fixed and rely on widening and narrowing operations. In this talk, I present a predictable abstract-interpretation based technique for computing numerical loop summaries. The technique works by first synthesizing a rational vector addition system with resets (Q-VASR) that simulates the action of an input loop, and then uses the (polytime computable) reachability relation of Q-VASRs to over-approximate the behavior of the loop. The key contribution presented (and the crux behind the predictability claim) is the ability to synthesize a Q-VASR that is a best abstraction of a LRA loop in the sense that (1) it simulates the loop and (2) it is simulated by any other Q-VASR that simulates the loop. In addition, I present a technique for improving the precision of the analysis by using Q-VASR with states to capture loop control structure. These techniques have been benchmarked against state-of-the-art tools; experiments show that these techniques are both precise and performant. The reading list papers are C. Calcagno, D. Distefano, P. W. O’Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction, in: Proc. Symposium on Principles of Programming Languages (POPL ’09), pages 289–300. ACM Press, 2009. M. Colon, S. Sankaranarayanan, and H. Sipma, Linear invariant generation using non-linear constraint solving, in: International Conference on Computer-Aided Verification (CAV ‘03), pages 420–432 P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: Proc. Symposium on Principles of Programming Languages (POPL ‘77). ACM Press, New York, 1977. A. Farzan and Z. Kincaid. Compositional Recurrence Analysis. In: Proc Formal Methods in Computer-Aided Design (FMCAD ’15). C. Haase and S. Halfon. Integer vector addition systems with states. in Proc: International Workshop on Reachability Problems (RP ‘14), volume 8762 of Lecture Notes in Computer Science, pages 112–124. Springer, 2014 F. Konecny. PTIME computation of transitive closures of octagonal relations. in Proc: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016). K. L. McMillan. Lazy abstraction with interpolants. in: Proc International Conference on Computer-Aided Verification (CAV ‘06), pages 123–136. Springer-Verlag, Berlin, Germany, M. Müller-Olm and H. Seidl. Precise interprocedural analysis through linear algebra. in Proc: Symposium on Principles of Programming Languages (POPL ’04). T. Reps, S. Horwitz and M. Sagiv, Precise interprocedural dataflow analysis via graph reachability, in Proc: ACM Symposium on Principles of Programming Languages (POPL ‘95), pages 49-61. T. Reps, M. Sagiv, and G. Yorsh. Symbolic implementation of the best transformer. in Proc. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI ‘04). R. E. Tarjan, A unified approach to path problems, J. ACM, 28(3), 577–593 (1981). The reading list books are A.R. Bradley, Z. Manna. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007) F. Nielson, H. Riis Nielson, and C. Hankin, Principles of Program Analysis, Springer-Verlag, 1999.