Bibliography

Major publications by the team in recent years

1J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, X. Rival.

Static Analysis and Verification of Aerospace Software by Abstract Interpretation, in: Proceedings of the American Institue of Aeronautics and Astronautics (AIAA Infotech@Aerospace 2010), Atlanta, Georgia, USA, American Institue of Aeronautics and Astronautics, 2010.

http://hal.inria.fr/inria-00528611
2B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, 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), ACM Press, June 7–14 2003, p. 196–207.
3P. Cousot.

Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation, in: Theoretical Computer Science, 2002, vol. 277, n^o 1–2, p. 47–103.
4J. Feret, V. Danos, J. Krivine, R. Harmer, W. Fontana.

Internal coarse-graining of molecular systems, in: Proceeding of the national academy of sciences, Apr 2009, vol. 106, n^o 16.

http://hal.inria.fr/inria-00528330
5L. Mauborgne, X. Rival.

Trace Partitioning in Abstract Interpretation Based Static Analyzers, in: Proceedings of the 14th European Symposium on Programming (ESOP'05), M. Sagiv (editor), Lecture Notes in Computer Science, Springer-Verlag, 2005, vol. 3444, p. 5–20.
6A. Miné.

The Octagon Abstract Domain, in: Higher-Order and Symbolic Computation, 2006, vol. 19, p. 31–100.
7X. Rival.

Symbolic Transfer Functions-based Approaches to Certified Compilation, in: Conference Record of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, United States, 2004, p. 1–13.

Publications of the year

Doctoral Dissertations and Habilitation Theses

8X. Rival.

Abstract domains for the analysis of programs manipulating complex data-structures, École Normale Supérieure, June 2011, Habilitation à Diriger des Recherches.

Articles in International Peer-Reviewed Journal

9J. Bertrane, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, X. Rival.

Static analysis by abstract interpretation of embedded critical software, in: ACM SIGSOFT Software Engineering Notes, 2011, vol. 36, n^o 1, p. 1-8.
10A. Cortesi, M. Zanioli.

Widening and narrowing operators for abstract interpretation, in: Computer Languages, Systems and Structures, 2011, vol. 37, n^o 1, p. 24 - 42.

http://dx.doi.org/10.1016/j.cl.2010.09.001
11P. Cousot, R. Cousot.

Grammar semantics, analysis and parsing by abstract interpretation, in: Theoretical Computer Science, 2011, vol. 412, n^o 44, p. 6135-6192.
12J. Feret, T. Henzinger, H. Koeppl, T. Petrov.

Lumpability Abstractions of Rule-based Systems, in: Theorerical Computer Science, 2012, to appear.

http://dx.doi.org/10.1016/j.tcs.2011.12.059

Invited Conferences

13F. Camporesi, J. Feret.

Formal reduction for rule-based models, in: Post-proceedings of the the 27th Conference on the Mathematical Foundations of Programming Semantics - (MFPS'11), Pittsburgh, United States, M. Mislove, J. Ouaknine (editors), Electronic Notes in Theoretical Computer Science, Elsevier, September 2011, vol. 276, p. 29-59. [ DOI : 10.1016/j.entcs.2011.09.014 ]

http://hal.inria.fr/inria-00636850/en
14J. Feret.

Formal Model Reduction, in: Proceedings of the 18th International Static Analysis Symposium (SAS'11), Venice, Italy, E. Yahav (editor), Lecture Notes in Computer Science, 2011, vol. 6887, p. 6–6. [ DOI : 10.1007/978-3-642-23702-7_5 ]

http://hal.inria.fr/inria-00626640/en

International Conferences with Proceedings

15L. Chen, A. Miné, J. Wang, P. Cousot.

Linear Absolute Value Relation Analysis, in: Proceedings of the 20th European Symposium on Programming (ESOP'11), G. Barthe (editor), Lecture Notes in Computer Science, Springer, 2011, vol. 6602, p. 156–175.

http://hal.inria.fr/hal-00648039/
16A. Cortesi, M. Zanioli.

Information Leakage Analysis by Abstract Interpretation, in: Proceedings of the 37th International Conference on Current Trends in Theory and Practice of Computer Science, Novy Smokovec Slovakia, Lecture Notes in Computer Science, Springer, 2011, vol. 6543, p. 545–557.
17P. Cousot, R. Cousot.

An Abstract Interpretation Framework for Termination, in: Proceedings of the 39th Annual ACM Symposium on Principles Of Programming Languages (POPL'12), Philadelphia, PA, ACM Press, January 25–27 2012.
18P. Cousot, R. Cousot, F. Logozzo.

A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis, in: Proceedings of the 38th Annual ACM Symposium on Principles Of Programming Languages (POPL'11), Austin, Texas, United States, ACM Press, 2011.

http://hal.inria.fr/inria-00543874/en
19P. Cousot, R. Cousot, F. Logozzo.

Precondition Inference from Intermittent Assertions and Application to Contracts on Collections, in: Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Austin, Texas, United States, R. Jhala, D. Schmidt (editors), Springer-Verlag, 2011.

http://hal.inria.fr/inria-00543881/en
20P. Cousot, R. Cousot, L. Mauborgne.

The Reduced Product of Abstract Domains and the Combination of Decision Procedures, in: Proceedings of Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, M. Hofmann (editor), Lecture Notes in Computer Science, Springer, March-April 2011, vol. 6604, p. 456-472.
21P. Cousot, M. Monerau.

Probabilistic Abstract Interpretation, in: Proceedings of the 21th European Symposium on Programming (ESOP'12), H. Seidl (editor), Lecture Notes in Computer Science, Springer, March 2012, to appear.
22A. Miné.

Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs, in: Proceedings of the 20th European Symposium on Programming (ESOP'11), G. Barthe (editor), Lecture Notes in Computer Science, Springer, 2011, vol. 6602, p. 398–418.

http://hal.inria.fr/hal-00648038
23X. Rival, B.-Y. E. Chang.

Calling Contexts Abstraction with Shapes, in: Proceedings of the 38th Annual ACM Symposium on Principles Of Programming Languages (POPL'10), Austin, Texas, ACM Press, January 26–28, 2011.
24M. Zanioli, P. Ferrara, A. Cortesi.

SAILS: static analysis of information leakage with Sample, in: Proceedings of the 27th ACM Symposium on Applied Computing (SAC'12), Riva del Garda, Italy, ACM Press, 2012, to appear.

Scientific Books (or Scientific Book chapters)

25J. Bertrane, J. Feret, P. Cousot, R. Cousot, A. Miné, X. Rival, L. Mauborgne.

L'analyseur statique Astrée, in: Utilisations industrielles des techniques formelles : interprétation abstraite, J.-L. Boulanger (editor), Hermes-Lavoisier, June 2011, p. 67–113.

http://hal.inria.fr/inria-00636877/en

Books or Proceedings Editing

26J. Feret, A. Levchenko (editors)

Static Analysis and Systems Biology – 1st International Workshop, SASB 2010, Perpignan, France, September 13, 2010. PostProceedings, Electronic Notes in Theoretical Computer Science, Elsevier, 2011, vol. 272.

References in notes

27P. Cousot.

Proving the Absence of Run-Time Errors in Safety-Critical Avionics Code, invited tutorial, in: Proceedings of the Seventh ACM & IEEE International Conference on Embedded Software, EMSOFT'2007, C. M. Kirsch, R. Wilhelm (editors), ACM Press, New York, USA, 2007, p. 7–9.
28P. Cousot.

Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes (in French), Université scientifique et médicale de Grenoble, Grenoble, France, 21 March 1978.
29R. Cousot.

Reasoning about program invariance proof methods, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980, n^o CRIN-80-P050.
30P. Cousot.

Semantic Foundations of Program Analysis, in: Program Flow Analysis: Theory and Applications, S. S. Muchnick, N. D. Jones (editors), Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981, chap. 10, p. 303–342.
31R. Cousot.

Proving invariance properties of parallel programs by backward induction, University Paul Verlaine, Metz, France, March 1981, n^o LRIM-82-02.
32R. Cousot.

Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles (in French), Institut National Polytechnique de Lorraine, Nancy, France, 21 November 1985.
33P. Cousot.

The Calculational Design of a Generic Abstract Interpreter, invited chapter, in: Calculational System Design, M. Broy, R. Steinbrüggen (editors), NATO Science Series, Series F: Computer and Systems Sciences. IOS Press, Amsterdam, The Netherlands, 1999, vol. 173, p. 421–505.
34P. Cousot, R. Cousot.

Basic Concepts of Abstract Interpretation, invited chapter, in: Building the Information Society, R. Jacquart (editor), Kluwer Academic Publishers, Dordrecht, The Netherlands, 2004, chap. 4, p. 359–366.
35P. Cousot, R. Cousot.

Grammar Analysis and Parsing by Abstract Interpretation, invited chapter, in: Program Analysis and Compilation, Theory and Practice: Essays dedicated to Reinhard Wilhelm on the Occasion of his 60th Birthday, T. W. Reps, M. Sagiv, J. Bauer (editors), Lecture Notes in Computer Science, Springer, Berlin, Germany, 2007, vol. 4444.
36P. Cousot, R. Cousot.

Bi-inductive structural semantics, in: Information and Computation, 2009, vol. 207, n^o 2, p. 258–283.
37P. Cousot, 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, ACM Press, New York, United States, 1977, p. 238–252.
38P. Cousot, R. Cousot.

Systematic design of program analysis frameworks, in: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, ACM Press, New York, NY, USA, 1979, p. 269–282.
39P. Cousot, R. Cousot.

Semantic analysis of communicating sequential processes, in: Seventh International Colloquium on Automata, Languages and Programming, J. W. de Bakker, J. van Leeuwen (editors), Lecture Notes in Computer Science 85, Springer-Verlag, Berlin, Germany, July 1980, p. 119–133.
40P. Cousot, R. Cousot.

Invariance Proof Methods and Analysis Techniques For Parallel Programs, in: Automatic Program Construction Techniques, A. W. Biermann, G. Guiho, Y. Kodratoff (editors), Macmillan, New York, New York, United States, 1984, chap. 12, p. 243–271.
41P. Cousot, R. Cousot.

Higher-Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection and PER Analysis of Functional Languages), invited paper, in: Proceedings of the 1994 International Conference on Computer Languages, Toulouse, France, IEEE Computer Society Press, Los Alamitos, California, 16–19 May 1994, p. 95–112.
42P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival.

The Astrée analyser, in: Proceedings of the Fourteenth European Symposium on Programming Languages and Systems, ESOP'2005, Edinburg, Scotland, M. Sagiv (editor), Lecture Notes in Computer Science, Springer, Berlin, Germany, 2–10 April 2005, vol. 3444, p. 21–30.
43P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, X. Rival.

Varieties of Static Analyzers: A Comparison with Astrée , invited paper, in: Proceedings of the First IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE'07, Shanghai, China, M. Hinchey, J. He, J. Sanders (editors), IEEE Computer Society Press, Los Alamitos, California, USA, 6–8 June 2007.
44P. Cousot, R. Cousot, R. Giacobazzi.

Abstract Interpretation of Resolution-Based Semantics, in: Theoretical Computer Science, Nov. 2009, vol. 410, n^o 46.
45V. Danos, J. Feret, W. Fontana, R. Harmer, J. Krivine.

Abstracting the differential semantics of rule-based models: exact and automated model reduction, in: Proceedings of Logic in Computer Science (LICS 2010), Edinburgh, UK, J.-P. Jouannaud (editor), 2010, p. 362–381.

http://hal.inria.fr/hal-00520112, http://hal.inria.fr/hal-00520112
46V. Danos, J. Feret, W. Fontana, R. Harmer, J. Krivine.

Rule-based modelling of cellular signalling, in: Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07), Portugal, September 2007, vol. 4703, p. 17–41.

http://hal.archives-ouvertes.fr/hal-00164297/en/
47V. Danos, J. Feret, W. Fontana, J. Krivine.

Scalable Simulation of Cellular Signaling Networks, in: Proceedings of the 5th Asian Symposium on Programming Languages and Systems - APLAS'07, Z. Shao (editor), Lecture Notes in Computer Science, Springer, 2007, vol. 4807, p. 139-157. [ DOI : 10.1.1.139.5120 ]

http://hal.inria.fr/inria-00528409/en/
48V. Danos, J. Feret, W. Fontana, J. Krivine.

Abstract Interpretation of Cellular Signalling Networks, in: Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation - VMCAI'08, F. Logozzo, D. A. Peled, L. D. Zuck (editors), Lecture Notes in Computer Science, Springer, 2008, vol. 4905, p. 83-97. [ DOI : 10.1007/978-3-540-78163-9_11 ]

http://hal.inria.fr/inria-00528352/en/
49V. Danos, C. Laneve.

Formal Molecular Biology, in: Theoretical Computer Science, 10 2004, vol. 325, n^o 1, p. 69-110. [ DOI : 10.1016/j.tcs.2004.03.065 ]

http://hal.archives-ouvertes.fr/hal-00164591/en/
50R. Harmer, V. Danos, J. Feret, J. Krivine, W. Fontana.

Intrinsic Information carriers in combinatorial dynamical systems, in: Chaos, 2010, vol. 20, n^o 3, 037108 p.

http://hal.inria.fr/hal-00520128, http://hal.inria.fr/hal-00520128

Previous |

Home