Tutorial Speaker
Patrick Cousot is the inventor with Radhia Cousot, of Abstract Interpretation (1975), an influential technique in formal methods. He has been Professor of Computer Science at the École Normale Supérieure (ENS) in Paris since 1991. Currently, Patrick Cousot is a Professor of Computer Science at New York University. He is a knight (Chevalier) in the Ordre National du Mérite and the Ordre des Palmes académiques. In 1999 he received the CNRS Silver medal and in 2006 the great prize of the EADS Foundation. In 2001, he was bestowed an honorary doctorate by Saarland University, Germany. With Radhia Cousot, he received the ACM SIGPLAN Programming Languages Achievement Award in 2013 and the IEEE Computer Society Harlan D. Mills award in 2014, “For the invention of ‘abstract interpretation’, development of tool support, and its practical application”.
Abstract
We define the structural rule-based and then fixpoint prefix trace semantics of a simple subset of C. We define program properties and the strongest collecting semantics.
We formalize the exact abstraction of program properties and how a structural rule-based/fixpoint abstract semantics can be derived from the collecting semantics by calculational design. This is applied to program verification methods and program logics which are (non-computable) abstractions of the program collecting semantics.
Static analysis is based on the approximation of program properties. We introduce a few classical effectively computable abstractions of numerical properties of programs and shortly discuss industrial static analysis applications. We also consider a few abstractions of symbolic properties of programs and discuss opened problems.
Invited Talk
Sylvie Putot (Ecole Polytechnique, France). Zonotopic abstract domains for numerical program analysis.
Abstract. This lecture is a survey of the use of a generic abstract domain, based on zonotopes or affine forms, for the analysis of numerical programs, essentially control programs such as the ones found in the aerospace, nuclear and automotive industry.
This abstraction is well suited for representing and propagating perturbations, so that it can be used to deal both with real number and finite precision semantics. It is used in particular in the FLUCTUAT static analyzer to prove some functional properties of programs, generate (counter-) examples, identify the discrepancy between the real number and the finite precision semantics and its origin. It can also used as a basis for probabilistic static analyses. Recently, is has also been successfully used to analyze the safety and robustness of neural networks.
Bio. Sylvie Putot is Professor in the Department of Computer Science of Ecole Polytechnique. Her research focuses on set-based methods and abstractions for the verification of numerical programs and more generally cyber-physical systems. She is also one of the main authors of the Fluctuat static analyzer, dedicated to the analysis of floating-point programs.