Patrick Cousot, Abstract interpretation: from principles to application

Patrick Cousot.
Abstract interpretation: from principles to application
J.P. Morgan Chase Distinguished Lecture Series, Wednesday, June 30^th, 2021.
Slides of the 50mn talk:
- A4, 1 slide per landscape page, 11.3 Mb,
- Video of the remote talk
- Abstract:
     Abstract interpretation has been used for the design of program semantics, verification and sand methods of abstract interpretation (and compare it to other formal methods).
     Then we will sketch a lightweight formalization of program verification and analysis by abstract interpretation, in particular to discuss the concepts of soundness and completeness.
     Since program verification or analysis is undecidable, it cannot be automatized without compromise. Most academic and commercial analyser and unsound, incomplete, and may never terminate (they miss errors, may tag correct code as erroneous, and each run on the same program may report new errors, not reported earlier).
     In contrast, the main choices in static analysis by abstract interpretation are soundness (any claim of the static analyzer is always correct), termination (the analysis is always guaranteed to provide all answers in finite time), and incompleteness (some questions cannot be answered by the static analyzer and receive the correct but imprecise answer ``I don' know''). The main practical objective is therefore to have a good precision at a reasonable cost.
     Next, we will illustrate the use of static analysis to check a few basic examples of software safety and security requirements or find bugs.
     We will provide examples of sound static analyzers for the C/C++ language, mainly Astrée (https://www.absint.com/astree/index.htm) used in the safety critical industry (aviation, automobile, energy, space, communication, etc.).
     In conclusion, we will consider hot topics in abstract interpretation on today's trendy problematics of computer science and provide basic references.
- Keywords:
  Abstract Interpretation, Static analysis, Static analyzers.
- Bibliographic reference:
```
@unpublished{JPMorgan-2021-06-30-talk,
  author = {Patrick Cousot},
  title  = {Abstract interpretation: from principles to applications},
  note   = {J.P. Morgan Chase Distinguished Lecture Series},
  year   = {Wednesday, June 302 , 2021},
}
```
copyright notice
Last modified: Tue Jun 22 17:52:37 EDT 2021