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

  1. Jérôme Feret

Timetable

Monday, 18th15h-17hInformal introduction to Abstract Interpretation
Tuesday, 19th9h30-12h30The astrée analyzer
 14h-17h 
Wednesday, 20th9h30-12h30Static analysis of mobile systems
 14h-17h 
Thursday, 21st9h30-12h30Static analysis of biomolecular networks
 14h-17h 

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

  1. 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.

  2. 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 run-time 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].

  3. 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 non-uniform 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 Meta-language, which can be used to encode several model of mobility such as the pi-calculus [36], the ambient calculus [8], the spi-calculus [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 pi-calculus [20], and the one for the ambient calculus [19] can be tested on-line.

  4. Static analysis of biomolecular networks.

    Kappa [17, 18] is a site-graph rewrite systems which can be used to model protein-protein 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 over-approximates the set of reachable species which can be formed at run-time [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 plat-form.

    • 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 self-consistent portions of chemical species, called fragments, the behaviour of which can be described in a self-consistent way.
      • We will describe the fragment framework for reducing the differential semantics of rule-based models [32, 35, 15].
      • If we have time, we will describe the equivalent framework for reducing the stochastic semantics of rule-based 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 special-purpose static program analyzer for safety-critical real-time 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. Springer-Verlag, 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 safety-critical 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 rules-based 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 Twenty-sixth 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 SIGPLAN-SIGACT 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. Springer-Verlag, 2005.
[14]
Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, and Jean Krivine. Openkappa: a platform for rule-based models. http://www.kappalanguage.org/.
[15]
Vincent Danos, Jérôme Feret, Walter Fontana, Russell Harmer, and Jean Krivine. Abstracting the differential semantics of rule-based models: exact and automated model reduction. In Jean-Pierre Jouannaud, editor, Proceedings of the Twenty-Fifth 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. Springer-Verlag, April 2003.
[18]
Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoretical Computer Science, 325(1):69–110, September 2004.
[19]
J. Feret. Amb-s.a: a static analyzer for the pi-calculus. https://www.di.ens.fr/~feret/prototypes/ambsa.
[20]
J. Feret. Pi-s.a: a static analyzer for the pi-calculus. https://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. Springer-Verlag, 2000.
[24]
Jérôme Feret. Abstract interpretation-based static analysis of mobile ambients. In Eighth International Static Analysis Symposium (SAS’01), number 2126 in LNCS. Springer-Verlag, 2001.
[25]
Jérôme Feret. Occurrence counting analysis for the pi-calculus. 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. Springer-Verlag, 2002.
[27]
Jérôme Feret. Static analysis of digital filters. In European Symposium on Programming (ESOP’04), number 2986 in LNCS. Springer-Verlag, 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 arithmetic-geometric progression abstract domain. In Verification, Model Checking and Abstract Interpretation (VMCAI’05), number 3385 in LNCS, pages 42–58. Springer-Verlag, 2005.
[30]
Jérôme Feret. Numerical abstract domains for digital filters, 2005.
[31]
Jérôme Feret. Fragements-based 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 coarse-graining 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 rule-based 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 Join-Calculus: 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 LATEX by HEVEA.