Patrick Cousot (NYU University) will teach a course about the principles of abstract interpretation at the University of Venice from May, 23rd to May, 27th. Please fill the online form to sign up and attend the course (in person or remotely). In addition, the CSV Workshop on May, 20th is part of the course and it will be a prologue to the lectures given by prof. Cousot.

Course description

Modern societies are increasingly dependent upon the proper functioning of computer systems. Yet, computer programs are riddled with flaws that at best are inconvenient and annoying, and at worst, have extremely damaging consequences. Formal methods aim at using the rigor of mathematics for the specification, development, and verification of reliable and robust software and hardware systems. The ultimate objective of formal methods is to verify the correctness of computer systems and to have this verification completely automated, using computers. This objective is hard to achieve because of undecidability: no computer can correctly answer with finite time and memory resources every question relative to the correctness of an arbitrary computer system. Therefore all automated formal methods that provide answers in finite time on undecidable questions have to make compromises to escape this inevitable limitation of the power of computer systems:

  • Deductive methods based on automated theorem proving requires human guidance and assistance, which may be an overwhelming task;
  • Model-checking can only enumerate the behaviours of finite systems, and small enough to avoid time and memory explosion;
  • Static program analysis may be unsound or correct but not be precise enough to answer the desired questions.

The principles of abstract interpretation establish the foundations of all formal methods, their design, (un)soundness and (in)completeness, relative to the semantics of a programming language. The course formalizes exact and approximate semantic property abstraction with three main applications:

  • Semantics of programming languages (formally defining the possible executions of a program);
  • Design of deductive methods by abstract interpretation;
  • Design of static analysis by abstract interpretation.

The course has 5 days each with 4 academic hours (of 45 minutes). Electronic slides as well as notes will be provided. The notes include the mathematical prerequisites and contain additional material for further study.

Schedule

When Where Topic
Friday, May 20th 10:00-18:00 Aula Baratto, Main building CSV workshop  
Monday, May 23rd 11:00-12:30 Aula D, Zeta building, Scientific campus Semantics (part 1)
Monday, May 23rd 14:30-16:00 Aula D, Zeta building, Scientific campus Semantics (part 2)
Tuesday, May 24th 11:00-12:30 Aula D, Zeta building, Scientific campus Semantics (part 3)
Tuesday, May 24th 14:30-16:00 Aula D, Zeta building, Scientific campus Verification (part 1)
Wednesday, May 25th 11:00-12:30 Aula D, Zeta building, Scientific campus Verification (part 2)
Wednesday, May 25th 14:30-16:00 Aula D, Zeta building, Scientific campus Static analysis (part 1)
Thursday, May 26th 11:00-12:30 Aula D, Zeta building, Scientific campus Static analysis (part 2)
Thursday, May 26th 14:30-16:00 Aula D, Zeta building, Scientific campus Static analysis (part 3)
Friday, May 27th 11:00-12:30 Aula D, Zeta building, Scientific campus Static analysis (part 4)
Friday, May 27th 14:30-16:00 Aula D, Zeta building, Scientific campus Static analysis (part 5)

Exam

The final exam will consist in a seminar presenting a scientific paper about the application of the abstract interpretation theory to some contexts. A list of possible papers will be published in this webpage during the course.