Patrick Cousot, Dynamic abstract interpretation

Patrick Cousot.
Dynamic abstract interpretation
Invited Talk at SOAP at PLDI 2021, Tuesday, June 22^nd, 2021.
Slides of the 55mn talk:
- A4, 1 slide per landscape page, 1.2 Mb,
Abstract:
Abstract interpretation has been used for the design of program semantics, verification and static analysis methods, including typing. We show that abstract interpretation can also be used for dynamic static analysis, at run-time, during program execution, by formalizing all possible instrumented executions and proving their sound relationship with the program semantics.
We take the example of Ramon E. Moore's interval arithmetics used to put bounds on rounding errors and measurement errors in mathematical computations. Reals are represented by an interval of two floats guaranteed to contain this real. For tests and loops both true and false alternatives may be taken while only one would be taken with reals so that the instrumented semantics must be nondeterministic to be sound and is in general incomplete.
Keywords:
Dynamic analysis, Static analysis, Abstract Interpretation, Interval arithmetics.

Bibliographic reference:

@inproceedings{PCousot-SOAP-2021,
  author    = {Patrick Cousot},
  title     = {Dynamic abstract interpretation},
  booktitle = {10th ACM SIGPLAN International Workshop on the State of the Art in Program Analysis},
  year      = {Tuesday, June 22 , 2021},
  editor    = {Caterina Urban and Lisa Nguyen Quang Do},
  publisher = {ACM},
 }

copyright notice
Last modified: Tue Jun 22 17:52:37 EDT 2021