# Special Topics in Artificial Intelligence

## Theorem Proving for Program Analysis/Synthesis

Advanced course of the PhD program in "Computer Science": open to all students enrolled in the PhD program, regardless of year of enrollment. "Advanced" distinguishes it from the "basic" courses that the PhD program shares with the Master (Laurea magistrale) program.

Instructor: Maria Paola Bonacina
Office hours: Thursday 14:30 - 16:30, Room 1.73, Ca' Vignal 2.

Class meetings: Wednesday (except Thursday April 28 and May 5) 16:30-18:30 (13:30-15:30 on May 5) in room I (except March 9 in room F and May 5 in room C) from March 2 through May 18 (12 meetings).

Objective and motivation:
this advanced seminar will be an opportunity to study some theorem proving techniques used for program analysis or synthesis. In principle, program verification means proving programs correct, and program generation means generating automatically provably correct programs. In practice, a program analyzer helps the programmer by finding bugs, and a program synthesizer helps its user, who might not be a professional programmer, by generating executable code from constraints expressing user intent. There is a variety of methods to approach analysis or synthesis of programs. Several of them, and especially for the more difficult tasks, require theorem proving support, that is the capability of determining the validity of statements. For instance, a verifying compiler takes as input an annotated program and produces verification conditions that need to be proved valid to establish that the program satisfies its annotations. Another kind of analyzer takes as input a partially annotated program and produces the missing invariants, outsourcing to a theorem prover the task of determining the validity of auxiliary formulae generated in the process. A theorem prover applied in these contexts needs to be a decision procedure for decidable fragments of theories, generate proofs or counter-models, and extract interpolants from proofs. In current research, the border between program analyzer and theorem prover is getting thinner, as the theorem prover itself becomes capable of generating candidate invariants by interpolation, and dually the analyzer itself is seen as a kind of proof system. This seminar will be an opportunity to start exploring these research topics.

Class activity:
the course will start with a block of lectures by the instructor to provide the necessary background and conceptual framework, including decision procedures for selected theories, combination of theories by equality sharing (also known as Nelson-Oppen method), and basic notions on advanced topics such as interpolation of formulae. Then there will be presentations of papers by students, each followed by a discussion. These presentations, together with class participation, will also be the basis for students' evaluation.

Paper presentation and discussion:

• Wednesday, March 30: Claudio Tomazzoli:
• Vijay D’Silva, Daniel Kroening, Mitra Purandare and Georg Weissenbacher. Interpolant Strength. In the Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS 5944:129-145, Springer, 2010.
• Wednesday, April 6: Rosario Lombardo:
• Angelo Brillout, Daniel Kroening, Philipp Ruemmer, Thomas Wahl. An interpolating sequent calculus for quantifier-free Presburger arithmetic. In the Proceedings of the Fifth International Joint Conference on Automated Reasoning (IJCAR), LNAI 6173:384–399, Springer 2010.
• Wednesday, April 13: Durica Nikolic:
• Saurabh Srivastava, Sumit Gulwani and Jeffrey S. Foster. From program verification to program synthesis. In the Proceedings of the Thirty-First ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM Press, 2010.
• Wednesday, April 20: Alberto Calvi:
• Deepak Kapur, Rupak Majumdar and Calogero G. Zarba. Interpolation for data structures. In the Proceedings of the Fourteenth ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), ACM Press, 2006.
• Thursday, April 28: Erisa Karafili:
• Ken L. McMillan. Interpolation and SAT-based model checking. In the Proceedings of the Fifteenth Conference on Computer Aided Verification (CAV), LNCS 2725:1–13, Springer, 2003.
• Thursday, May 5: Marco Rocchetto:
• Ken L. McMillan. Lazy annotation for program testing and verification. In the Proceedings of the Twenty-second Conference on Computer Aided Verification (CAV), LNCS 6174:104–118, Springer 2010.
• Wednesday, May 11: Simone Marchesini:
• Greta Yorsh and Madanlal Musuvathi. A combination method for generating interpolants. In the Proceedings of the Twentieth Conference on Automated Deduction (CADE), LNAI 3632:353-368, Springer, 2005.
• Wednesday, May 18: Zhiyang Ong
• Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani. Efficient interpolant generation in satisfiability modulo a theory. In the Proceedings of the Fourteenth Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), LNCS 4963:397-412, Springer 2008.
• Alessandro Cimatti, Alberto Griggio and Roberto Sebastiani. Interpolation generation for UTVPI*. In the Proceedings of the Twenty-second Conference on Automated Deduction (CADE), LNAI 5663:167-182, Springer 2009.