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 Institute of Aeronautics and Astronautics (AIAA Infotech@Aerospace 2010), Atlanta, Georgia, USA, American Institute 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, pp. 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, pp. 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, pp. 5–20.
• 6A. Miné.
  
  The Octagon Abstract Domain, in: Higher-Order and Symbolic Computation, 2006, vol. 19, pp. 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, pp. 1–13.

Publications of the year

Doctoral Dissertations and Habilitation Theses

• 8A. Miné.
  
  Analyse statique par interprétation abstraite de programmes concurrents, Ecole Normale Supérieure de Paris - ENS Paris, November 2013, Habilitation à Diriger des Recherches.
  
  http://hal.inria.fr/tel-00903447

Articles in International Peer-Reviewed Journals

• 9A. Miné.
  
  Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions, in: Science of Computer Programming, October 2013. [ DOI : 10.1016/j.scico.2013.09.014 ]
  
  http://hal.inria.fr/hal-00903628

Invited Conferences

• 10P. Cousot, R. Cousot.
  
  A galois connection calculus for abstract interpretation, in: POPL - 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - 2014, San Diego, United States, S. Jagannathan, P. Sewell (editors), ACM, 2014, pp. 3-4. [ DOI : 10.1145/2535838.2537850 ]
  
  http://hal.inria.fr/hal-00930103

International Conferences with Proceedings

• 11M. Barnett, M. Bouaziz, F. Logozzo, M. Fähndrich.
  
  A case for static analyzers in the cloud, in: Bytecode - 8th Workshop on Bytecode Semantics, Verification, Analysis, and Transformation, Rome, Italy, M. Gomez-Zamalloa, G. Puebla (editors), ENTCS, Elsevier, 2014, to appear.
  
  http://hal.inria.fr/hal-00925837
• 12F. Camporesi, J. Feret, J. Hayman.
  
  Context-sensitive flow analyses: a hierarchy of model reductions, in: CMSB - 11th Conference on Computational Methods in Systems Biology - 2013, Klosterneuburg, Austria, A. Gupta, T. A. Henzinger (editors), Lecture Notes in BioInformatics, Springer, 2013, vol. 8130, pp. 220-233. [ DOI : 10.1007/978-3-642-40708-6_17 ]
  
  http://hal.inria.fr/hal-00846893
• 13B.-Y. E. Chang, X. Rival.
  
  Modular Construction of Shape-Numeric Analyzers, in: Festschrift for Dave Schmidt, Manhattan, Kansas, United States, A. Banerjee, O. Danvy, K.-G. Doh, J. Hatcliff (editors), EPTCS, September 2013, vol. 129.
  
  http://hal.inria.fr/hal-00926948
• 14P. Cousot, R. Cousot, M. Fähndrich, F. Logozzo.
  
  Automatic Inference of Necessary Preconditions, in: VMCAI 2013 - 14th Conference on Verification, Model Checking and Abstract Interpretation, Rome, Italy, R. Giacobazzi, J. Berdine, I. Mastroeni (editors), LNCS - Lecture Notes in Computer Science, Springer, 2013, vol. 7737, pp. 128-148. [ DOI : 10.1007/978-3-642-35873-9_10 ]
  
  http://hal.inria.fr/hal-00930070
• 15J. Hayman.
  
  Filtered compression for Kappa, in: SASB - 4th INternational Workshop on Static Analysis and Systems Biology, Seattle, United States, J. Feret, A. Levchenko (editors), Elsevier, 2014, to appear.
  
  http://hal.inria.fr/hal-00925549
• 16J. Hayman, T. Heindel.
  
  Pattern Graphs and Rule-Based Models: The Semantics of Kappa, in: FOSSACS - 16th International Conference on Foundations of Software Science and Computation Structures, Rome, Italy, F. Pfenning (editor), Lecture Notes in Computer Science, Springer, 2013, vol. 7794, pp. 1–16. [ DOI : 10.1007/978-3-642-37075-5 ]
  
  http://hal.inria.fr/hal-00925345
• 17A. Miné.
  
  Relational thread-modular static value analysis by abstract interpretation, in: VMCAI 2014 - 15th International Conference on Verification, Model Checking, and Abstract Interpretation, San Diego, United States, K. McMillan, X. Rival (editors), Lecture Notes in Computer Science, Springer, January 2014, vol. 8318, pp. 39-58. [ DOI : 10.1007/978-3-642-54013-4_3 ]
  
  http://hal.inria.fr/hal-00925713
• 18M. Pelleau, A. Miné, C. Truchet, F. Benhamou.
  
  A Constraint Solver based on Abstract Domains, in: VMCAI 2013 - 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Rome, Italy, R. Giacobazzi, J. Berdine, I. Mastroeni (editors), Lecture Notes in Computer Science, Springer-Verlag, 2013, vol. 7737, pp. 434–454. [ DOI : 10.1007/978-3-642-35873-9_26 ]
  
  http://hal.inria.fr/hal-00785604
• 19M. Pelleau, A. Miné, C. Truchet, F. Benhamou.
  
  Un solveur de contraintes basé sur les domaines abstraits, in: 9èmes Journées Francophones de Programmation par Contraintes, Aix-en-Provence, France, June 2013, pp. 259-268.
  
  http://hal.inria.fr/hal-00925430
• 20A. Toubhans, B.-Y. E. Chang, X. Rival.
  
  Reduced Product Combination of Abstract Domains for Shapes, in: VMCAI 2013 : 14th International Conference on Verification, Model Checking and Abstract Interpretation, Rome, Italy, R. Giacobazzi, J. Berdine, I. Mastroeni (editors), Lecture Notes in Computer Science, Springer, January 2013, vol. 7737, pp. 375-395. [ DOI : 10.1007/978-3-642-35873-9_23 ]
  
  http://hal.inria.fr/hal-00760428
• 21O. Tripp, M. Pistoia, P. Cousot, R. Cousot, S. Guarnieri.
  
  Andromeda: Accurate and Scalable Security Analysis of Web Applications, in: FASE 2013 - International Conference Fundamental Approaches to Software Engineering, Rome, Italy, V. Cortellessa, D. Varró (editors), LNCS - Lecture Notes in Computer Science, Springer, 2013, vol. 7793, pp. 210-225, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013. [ DOI : 10.1007/978-3-642-37057-1_15 ]
  
  http://hal.inria.fr/hal-00930096
• 22C. Urban, A. Miné.
  
  An abstract domain to infer ordinal-valued ranking functions, in: 23rd European Symposium on Programming, Grenoble, France, Z. Shao (editor), Lecture Notes in Computer Science, Springer, April 2014.
  
  http://hal.inria.fr/hal-00925731
• 23C. Urban.
  
  Piecewise-Defined Ranking Functions, in: 13th International Workshop on Termination, Bertinoro, Italy, J. Waldmann (editor), August 2013, pp. 69-73.
  
  http://hal.inria.fr/hal-00925682
• 24C. Urban.
  
  The Abstract Domain of Segmented Ranking Functions, in: Static Analysis, 20th International Symposium,, Seattle, United States, F. Logozzo, M. Fähndrich (editors), Lecture Notes in Computer Science, Springer, June 2013, vol. 7935, pp. 43-62. [ DOI : 10.1007/978-3-642-38856-9_5 ]
  
  http://hal.inria.fr/hal-00925670

Books or Proceedings Editing

• 25R. Giacobazzi, R. Cousot (editors)
  
  Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, ACM, 2013, 574 p.
  
  http://hal.inria.fr/hal-00930257
• 26K. McMillan, X. Rival (editors)
  
  Verification, Model Checking, and Abstract Interpretation, Springer, 2014, vol. 8318, 493 p.
  
  http://hal.inria.fr/hal-00931694

Other Publications

• 27A. Atki.
  
  Implémentation du domaine asbtrait numérique TVPI pour APRON, École Polytechnique, Palaiseau, July 2013, 28 p.
  
  http://hal.inria.fr/hal-00925999
• 28M. Bry.
  
  Synchronisation de fils d'exécution en interprétation abstraite, École Polytechnique, Palaiseau, July 2013, 16 p.
  
  http://hal.inria.fr/hal-00926979
• 29C. Urban.
  
  Automatic Inference of Ranking Functions by Abstract Interpretation, January 2014, Student Poster Session, 41st Symposium on Principles of Programming Languages (POPL 2014).
  
  http://hal.inria.fr/hal-00925760

References in notes

• 30P. 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, pp. 7–9.
• 31P. 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, 21 March 1978.
• 32R. 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, 22 p.
• 33P. 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, pp. 303–342.
• 34R. Cousot.
  
  Proving invariance properties of parallel programs by backward induction, University Paul Verlaine, Metz, France, March 1981, n^o LRIM-82-02, 38 p.
• 35R. 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.
• 36P. 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, pp. 421–505.
• 37P. 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, pp. 359–366.
• 38P. 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.
• 39P. Cousot, R. Cousot.
  
  Bi-inductive structural semantics, in: Information and Computation, 2009, vol. 207, n^o 2, pp. 258–283.
• 40P. Cousot, R. Cousot.
  
  An Abstract Interpretation Framework for Termination, in: Conference Record of the 39 th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, ACM Press, New York, January 25-27 2012, pp. 245–258.
• 41P. 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, pp. 238–252.
• 42P. 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, pp. 269–282.
• 43P. 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, pp. 119–133.
• 44P. 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, pp. 243–271.
• 45P. 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, pp. 21–30.
• 46P. 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.
• 47P. Cousot, R. Cousot, R. Giacobazzi.
  
  Abstract Interpretation of Resolution-Based Semantics, in: Theoretical Computer Science, Nov. 2009, vol. 410, n^o 46.
• 48V. Danos, J. Feret, W. Fontana, R. Harmer, J. Hayman, J. Krivine, C. Thompson-Walsh, G. Winskel.
  
  Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models, in: 32nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), Hyderabad, India, D. D'Souza, J. Radhakrishnan, K. Telikepalli (editors), LIPIcs, December 2012.
  
  http://hal.inria.fr/hal-00734487
• 49V. 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, pp. 362–381.
  
  http://hal.inria.fr/hal-00520112, http://hal.inria.fr/hal-00520112
• 50V. 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, pp. 17–41.
  
  http://hal.archives-ouvertes.fr/hal-00164297/en/
• 51V. 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, pp. 139-157. [ DOI : 10.1.1.139.5120 ]
  
  http://hal.inria.fr/inria-00528409/en/
• 52V. 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, pp. 83-97. [ DOI : 10.1007/978-3-540-78163-9_11 ]
  
  http://hal.inria.fr/inria-00528352/en/
• 53V. Danos, C. Laneve.
  
  Formal Molecular Biology, in: Theoretical Computer Science, 10 2004, vol. 325, n^o 1, pp. 69-110. [ DOI : 10.1016/j.tcs.2004.03.065 ]
  
  http://hal.archives-ouvertes.fr/hal-00164591/en/
• 54J. Desharnais, R. Jagadeesan, V. Gupta, P. Panangaden.
  
  The Metric Analogue of Weak Bisimulation for Probabilistic Processes, in: LICS, IEEE Computer Society, 2002, pp. 413-422.
• 55J. Feret.
  
  Static Analysis of Digital Filters, in: European Symposium on Programming (ESOP'04), LNCS, Springer-Verlag, 2004, n^o 2986, pp. 33–48, © Springer-Verlag.
• 56J. Feret.
  
  Numerical Abstract Domains for Digital Filters, in: International workshop on Numerical and Symbolic Abstract Domains (NSAD 2005), 2005.
• 57N. Ferns, P. Panangaden, D. Precup.
  
  Bisimulation Metrics for Continuous Markov Decision Processes, in: SIAM J. Comput., 2011, vol. 40, n^o 6, pp. 1662-1714.
• 58R. Harmer, V. Danos, J. Feret, J. Krivine, W. Fontana.
  
  Intrinsic Information carriers in combinatorial dynamical systems, in: Chaos, 2010, vol. 20, n^o 3.
  
  http://hal.inria.fr/hal-00520128, http://hal.inria.fr/hal-00520128
• 59A. Müller.
  
  Integral probability metrics and their generating classes of functions, Discussion paper, Inst. für Wirtschaftstheorie und Operations Research, 1995.
  
  http://books.google.fr/books?id=ZYNYtwAACAAJ
• 60F. van Breugel, J. Worrell.
  
  An Algorithm for Quantitative Verification of Probabilistic Transition Systems, in: CONCUR, K. G. Larsen, M. Nielsen (editors), Lecture Notes in Computer Science, Springer, 2001, vol. 2154, pp. 336-350.
• 61F. van Breugel, J. Worrell.
  
  Towards Quantitative Verification of Probabilistic Transition Systems, in: ICALP, F. Orejas, P. G. Spirakis, J. van Leeuwen (editors), Lecture Notes in Computer Science, Springer, 2001, vol. 2076, pp. 421-432.