Abstract interpretation and applications 
From 2011, April the 18th to April the 21st, Università di Bologna.
The exam set will be provided later (second week of May).
Goal
The goal of these lecture is to briefly introduce the Abstract Interpretation framework and to illustrate its applications in the design of some static analyses.
Speaker

Jérôme Feret
Timetable
Monday, 18th  15h17h  Informal introduction to Abstract Interpretation 
Tuesday, 19th  9h3012h30  The astrée analyzer 
 14h17h  
Wednesday, 20th  9h3012h30  Static analysis of mobile systems 
 14h17h  
Thursday, 21st  9h3012h30  Static analysis of biomolecular networks 
 14h17h  
Slides
Software
Preliminary requirements
This course requires no preliminary knowledge.
The fundamental notions which will be used in this course will be properly introduced.
Content

Informal introduction to abstract interpretation.
Abstract interpretation [10, 11, 9] is a unifying framework for the approximation of mathematical structure. During the week, we will use this framework to derive sound, automatic and terminating
analyzer to abstract the properties of interest of programs and systems.
We will start the week with a short introduction to abstract interpretation which is taken from some Lectures that Patrick Cousot gave at MIT in 2005.
 astrée: a static analyzer for certifying large embedded critical software.
Then, we will study the design of the astrée analyzer.
The astrée analyzer [3, 4, 5, 13, 2] is a static analyzer which aims at proving the absence of runtime errors (RTEs) in critical embedded software. It has been used successfully to certify fly by wire control command software of the AirBus A340 and A380, and the Jules Vernes Automated Transfer Vehicle (ATV) enabling ESA to transport payloads to the International Space Station.
First we will give an overview of the astrée analyzer .
Then we will detailed the design of two abstract numerical domains.

The first one uses arithmetic and geometric progressions to bound the contribution of rounding errors in arithmetic computations [29].
 The second targets the analysis of digital filtering algorithms, which are used to smooth streams of input values [27, 30]. It uses quadratic constraints (ellipses) and formal development.
If we have enough time, we will describe the model of collaboration between abstract domains and its interaction with the extrapolation of an inductive invariant [12].
 Static analysis of mobile systems.
A mobile system is a set of processes which interact with each other while modifying dynamically their capability of interaction [36].
The main difficulty is that the topology of interaction is dynamic and potentially infinite. Their analysis requires a precise approximation of the flow of the programs.
We propose three families of complementary analyses:

A nonuniform approximation of the interactions between components [23, 24, 26, 28, 21]
 A counting analysis which can detect which components can occur simultaneously [25, 28, 21]
 A analysis of the different sessions of the systems which is based of thread partitioning (which gathers the components interacting with each other, and counts the number of components within each equivalence class of components) [21].
All these analyses are defined on a Metalanguage, which can be used to encode several model of mobility such as the picalculus [36], the ambient calculus [8], the spicalculus [1], the join calculus [34], and so on and so forth, and thus, get an analyzer for each of these languages.
The static analyzer for the picalculus [20], and the one for the ambient calculus [19] can be tested online.
 Static analysis of biomolecular networks.
Kappa [17, 18] is a sitegraph rewrite systems which can be used to model proteinprotein interaction networks, in a compact and elegant way.
We propose several analyses so as to help the design of models, and compute their behaviour.

We propose a static analysis which overapproximates the set of reachable species which can be formed at runtime [22, 16]. This analysis helps the debugging of models by detecting dead rules and structural invariants about the biochemical composition of chemical species.
A problem set will be given so as to prove the main results of this framework.
Moreover, a practical work will be provided to test the different functionalities of the openkappa [14] modeling platform.
 We propose a model reduction framework to drastically reduce the combinatorial complexity of our systems. This framework tracks how different regions of chemical species may influence the behaviour of each other, and deduces a set of selfconsistent portions of chemical species, called fragments, the behaviour of which can be described in a selfconsistent way.

We will describe the fragment framework for reducing the differential semantics of rulebased models [32, 35, 15].
 If we have time, we will describe the equivalent framework for reducing the stochastic semantics of rulebased models [33, 31, 6].
We will also describe some algebraic primitive to combine model reductions [7].
The static analyzer complx can be downloaded on the openkappa site [14].
Local organizer
References

[1]

Martín Abadi and Andrew D. Gordon.
A calculus for cryptographic protocols: The spi calculus.
In Proc. CCS’97. ACM Press, 1997.
 [2]

J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, and
X. Rival.
An abstract domain to discover interval linear equalitiesstatic
analysis and verification of aerospace software by abstract interpretation.
In AIAA Infotech@Aerospace 2010, Atlanta, Georgia, 20–22 April
2010. American Institute of Aeronautics and Astronautics.
 [3]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A.
Miné, D. Monniaux, and X. Rival.
The astrée static analyzer.
http://www.astree.ens.fr.
 [4]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A.
Miné, D. Monniaux, and X. Rival.
Design and implementation of a specialpurpose static program
analyzer for safetycritical realtime embedded software, invited chapter.
In T. Mogensen, D.A. Schmidt, and I.H. Sudborough, editors,
The Essence of Computation: Complexity, Analysis, Transformation. Essays
Dedicated to Neil D. Jones, LNCS 2566, pages 85–108. SpringerVerlag,
October 2002.
 [5]

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A.
Miné, D. Monniaux, and X. Rival.
A static analyzer for large safetycritical software.
In Proceedings of the ACM SIGPLAN 2003 Conference on Programming
Language Design and Implementation (PLDI’03), pages 196–207, San Diego,
California, USA, June 7–14 2003. ACM Press.
 [6]

Ferdinanda Camporesi, Jérôme Feret, Heinz Koeppl, and Tatjana Petrov.
Automatic reduction of stochastic rulesbased models in a nutshell.
In T.E. Simos, editor, Proceedings of the International
Conference of Numerical Analysis and Applied Mathematics ICNAAM ’10,
number 1281 in American Institute of Physics Conference Proceedings, pages
1330–1334, Rhodes, Greece, 19–25 September 2010. American Institute of
Physics.
 [7]

Ferdinanda Camporesi, Jérôme Feret, Heinz Koeppl, and Tatjana Petrov.
Combining model reductions.
In Michael Mislove and Peter Selinger, editors, Postproceedings
of the Twentysixth Conference on the Mathematical Foundations of Programming
Semantics, MFPS XXVI, volume 265 of Electonic Notes in Theoretical
Computer Science, pages 73–96, Ottawa, Cabada, 6–10 May 2010. Elsevier
Science Publishers.
 [8]

Luca Cardelli and Andrew D. Gordon.
Mobile ambients.
Theoretical Computer Science, 240(1), 1998.
 [9]

P. Cousot.
The calculational design of a generic abstract interpreter.
In M. Broy and R. Steinbrüggen, editors, Calculational
System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.
 [10]

P. Cousot and R. Cousot.
Abstract interpretation: a unified lattice model for static analysis
of programs by construction or approximation of fixpoints.
In Conference Record of the Fourth Annual ACM SIGPLANSIGACT
Symposium on Principles of Programming Languages, pages 238–252, Los
Angeles, California, 1977. ACM Press, New York, NY.
 [11]

P. Cousot and R. Cousot.
Abstract interpretation frameworks.
Journal of Logic and Computation, 2(4):511–547, 1992.
 [12]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D.
Monniaux, and X. Rival.
Combination of abstractions in the astrée static analyzer.
In M. Okada and I. Satoh, editors, Eleventh Annual Asian
Computing Science Conference (ASIAN’06), Tokyo, Japan, LNCS 4435, 2007.
Springer, Berlin.
 [13]

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine
Miné, David Monniaux, and Xavier Rival.
The astrée analyzer.
In M. Sagiv, editor, European Symposium on Programming
(ESOP’05), volume 3444 of Lecture Notes in Computer Science, pages
21–30. SpringerVerlag, 2005.
 [14]

Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, and Jean
Krivine.
Openkappa: a platform for rulebased models.
http://www.kappalanguage.org/.
 [15]

Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, and Jean
Krivine.
Abstracting the differential semantics of rulebased models: exact
and automated model reduction.
In JeanPierre Jouannaud, editor, Proceedings of the
TwentyFifth Annual IEEE Symposium on Logic in Computer Science,
LICS ’2010, volume 0, pages 362–381, Edinburgh, UK, 11–14 July 2010.
IEEE Computer Society.
 [16]

Vincent Danos, Jérôme Feret, Walter Fontana, and Jean Krivine.
Abstract interpretation of cellular signalling networks.
In Francesco Logozzo, Doron A. Peled, and Lenore D. Zuck, editors,
Proceedings of the Ninth International Conference on Verification, Model
Checking and Abstract Interpretation, VMCAI ’2008, volume 4905 of Lecture Notes in Computer Science, pages 83–97, San Francisco, USA, 7–9
January 2008. Springer, Berlin, Germany.
 [17]

Vincent Danos and Cosimo Laneve.
Core formal molecular biology.
In Proc. ESOP’03, volume 2618 of LNCS. SpringerVerlag,
April 2003.
 [18]

Vincent Danos and Cosimo Laneve.
Formal molecular biology.
Theoretical Computer Science, 325(1):69–110, September 2004.
 [19]

J. Feret.
Ambs.a: a static analyzer for the picalculus.
http://www.di.ens.fr/~feret/prototypes/ambsa.
 [20]

J. Feret.
Pis.a: a static analyzer for the picalculus.
http://www.di.ens.fr/~feret/prototypes/pisa.
 [21]

J. Feret.
Analysis of Mobile Systems by Abstract Interpretation.
PhD thesis, Ecole Polytechnique, 2005.
 [22]

J. Feret.
Reachability analysis of biological signalling pathways by abstract
interpretation.
In T.E. Simos, editor, Proceedings of the International
Conference of Computational Methods in Sciences and Engineering,
ICCMSE ’2007, Corfu, Greece, number 963.(2) in American Institute of
Physics Conference Proceedings, pages 619–622, Corfu, Greece, 25–30
September 2007. American Institute of Physics.
 [23]

Jérôme Feret.
Confidentiality analysis of mobile systems.
In Seventh International Static Analysis Symposium (SAS’00),
number 1824 in LNCS. SpringerVerlag, 2000.
 [24]

Jérôme Feret.
Abstract interpretationbased static analysis of mobile ambients.
In Eighth International Static Analysis Symposium (SAS’01),
number 2126 in LNCS. SpringerVerlag, 2001.
 [25]

Jérôme Feret.
Occurrence counting analysis for the picalculus.
Electronic Notes in Theoretical Computer Science, 39.(2), 2001.
Workshop on GEometry and Topology in COncurrency theory, PennState,
USA, August 21, 2000.
 [26]

Jérôme Feret.
Dependency analysis of mobile systems.
In European Symposium on Programming (ESOP’02), number 2305 in
LNCS. SpringerVerlag, 2002.
 [27]

Jérôme Feret.
Static analysis of digital filters.
In European Symposium on Programming (ESOP’04), number 2986 in
LNCS. SpringerVerlag, 2004.
 [28]

Jérôme Feret.
Abstract interpretation of mobile systems.
J. Log. Algebr. Program., 63(1):59–130, 2005.
 [29]

Jérôme Feret.
The arithmeticgeometric progression abstract domain.
In Verification, Model Checking and Abstract Interpretation
(VMCAI’05), number 3385 in LNCS, pages 42–58. SpringerVerlag, 2005.
 [30]

Jérôme Feret.
Numerical abstract domains for digital filters, 2005.
 [31]

Jérôme Feret.
Fragementsbased model reduction: some case studies.
In Jean Krivine and Angelo Troina, editors, Préproceedings of
the First International Workshop on Interactions between Computer Science and
Biology, CS2Bio ’2010, Electonic Notes in Theoretical Computer Science,
Amsterdam, Netherlands, 10 June 2010. Elsevier Science Publishers.
 [32]

Jérôme Feret, Vincent Danos, Jean Krivine, Russ Harmer, and Walter Fontana.
Internal coarsegraining of molecular systems.
Proceedings of the National Acedemy of Sciences of the United
States of America, April 3 2009.
 [33]

Jérôme Feret, Thomas Henzinger, Heinz Koeppl, and Tatjana Petrov.
Lumpability abstractions of rulebased systems.
In M. Koutny G. Ciobanu, editor, Postproceedings of the 4th
Workshop on Membrane Computing and Biologically Inspired Process Calculi,
MeCBIC 10, Electronic Proceedings in Theoretical Computer Science, Jena,
Germany, 23 August 2010. Electronic Proceedings in Theoretical Computer
Science.
 [34]

Cédric Fournet.
The JoinCalculus: A Calculus for Distributed Mobile
Programming.
PhD thesis, École Polytechnique, Paris, France, 1998.
 [35]

Russ Harmer, Vincent Danos, Jérôme Feret, Jean Krivine, and Walter Fontana.
Intrinsic information carriers in combinatorial dynamical systems.
Chaos, 20, September 2010.
 [36]

Robin Milner, Joachim Parrow, and David Walker.
A calculus of mobile processes.
Information and Computation, 1992.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.