EN FR
EN FR
ABSTRACTION - 2012
ABSTRACTION - 2012




Project-Team Abstraction
Members
Overall Objectives
Scientific Foundations
Application Domains
Software
New Results
Bilateral Contracts and Grants with Industry
Partnerships and Cooperations
Dissemination
Bibliography




Project-Team Abstraction
Members
Overall Objectives
Scientific Foundations
Application Domains
Software
New Results
Bilateral Contracts and Grants with Industry
Partnerships and Cooperations
Dissemination
Bibliography


previous Previous | up Home


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, 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, no 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, no 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

  • 8M. Zanioli.

    Security Analysis by Abstract Interpretation, Université Paris VII and Università Ca'Foscari (Venice), March 2012.

Articles in International Peer-Reviewed Journals

  • 9E. J. Deeds, J. Krivine, J. Feret, V. Danos, W. Fontana.

    Combinatorial complexity and compositional drift in protein interaction networks., in: PLoS ONE, 2012, vol. 7, no 3. [ DOI : 10.1371/journal.pone.0032032 ]

    http://hal.inria.fr/hal-00677889
  • 10J. Feret, T. Henzinger, H. Koeppl, T. Petrov.

    Lumpability Abstractions of Rule-based Systems, in: Theoretical Computer Science, 2012, vol. 431, p. 137-164. [ DOI : 10.1016/j.tcs.2011.12.059 ]

    http://hal.inria.fr/hal-00677894
  • 11A. Miné.

    Static analysis of run-time errors in embedded real-time parallel C programs, in: Logical Methods in Computer Science, March 2012, vol. 8, no 1:26, 63 p.

    http://hal.inria.fr/hal-00748098

Invited Conferences

  • 12P. Cousot.

    Formal Verification by Abstract Interpretation., in: 4th NASA Formal Methods Symposium (NFM'12), Heidelberg, A. Goodloe, S. Person (editors), LNCS, Springer-Verlag, 2012.

    http://www.di.ens.fr/~cousot/publications.www/Cousot-NFM2012.pdf
  • 13T. Petrov, J. Feret, H. Koeppl.

    Reconstructing Species-Based Dynamics from Reduced Stochastic Rule-Based Models., in: Winter Simulation Conference (WSC'12), Berlin, Germany, C. Laroque, J. Himmelspach, R. Pasupathy, O. Rose, A. M. Uhrmacher (editors), December 2012.

    http://hal.inria.fr/hal-00734483

International Conferences with Proceedings

  • 14M. Bouaziz.

    TreeKs: A Functor to Make Numerical Abstract Domains Scalable, in: 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD'12), Deauville, France, ENTCS, Elsevier, September 2012, 12 p.

    http://dx.doi.org/10.1016/j.entcs.2012.09.005
  • 15M. Bouaziz, F. Logozzo, M. Fahndrich.

    Inference of Necessary Field Conditions with Abstract Interpretation, in: 10th Asian Conference on Programming Languages And Software (APLAS'12), Kyoto, Japon, LNCS, December 2012.

    http://research.microsoft.com/apps/pubs/default.aspx?id=172534
  • 16T. Cheng, X. Rival.

    An Abstract Domain to Infer Types over Zones in Spreadsheets, in: 19th Static Analysis Symposium (SAS'12), Deauville, France, LNCS, September 2012.

    http://hal.inria.fr/hal-00760424
  • 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.

    http://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL12-ACM-p245-258-2012.pdf
  • 18P. Cousot, R. Cousot, M. Fahndrich, F. Logozzo.

    The Design and Implementation of a System for the Automatic Inference of Necessary Preconditions, in: 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'13), Rome, Italie, LNCS, Springer, January 2013, to appear.
  • 19P. Cousot, M. Monerau.

    Probabilistic Abstract Interpretation, in: 22nd European Symposium on Programming (ESOP'12), Heidelberg, H. Seidel (editor), LNCS, Springer-Verlag, 2012.

    http://www.di.ens.fr/~cousot/publications.www/CousotMonerau-ESOP2012.pdf
  • 20V. 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
  • 21J. Hayman, T. Heindel.

    Pattern Graphs and Rule-Based Models: the semantics of Kappa, in: 16th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'13), Rome, Italy, LNCS, March 2013.
  • 22A. Miné.

    Abstract domains for bit-level machine integer and floating-point operations, in: 4th International Workshop on invariant Generation (WING'12), Manchester, Royaume-Uni, June 2012, 16 p.

    http://hal.inria.fr/hal-00748094
  • 23A. Miné.

    Inferring sufficient conditions with backward polyhedral under-approximations, in: 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD'12), Deauville, France, ENTCS, Elsevier, September 2012, 12 p.

    http://hal.inria.fr/hal-00748095
  • 24A. Miné.

    Static Analysis by Abstract Interpretation of Sequential and Multi-Thread Programs, in: 10th School of Modelling and Verifying Parallel Processes, Marseille, France, P.-A. Reynier (editor), December 2012.

    http://hal.inria.fr/hal-00763076
  • 25M. Pelleau, A. Miné, C. Truchet, F. Benhamou.

    A constraint solver based on abstract domains, in: 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'13), Rome, Italie, LNCS, Springer, January 2013, 17 p.

    http://hal.inria.fr/hal-00748096
  • 26P. Sotin, X. Rival.

    Hierarchical Abstraction of Dynamic Structures, in: 10th Asian Conference on Programming Languages And Software (APLAS'12), Kyoto, Japon, LNCS, December 2012.

    http://hal.inria.fr/hal-00760427
  • 27A. Toubhans, B.-Y. E. Chang, X. Rival.

    Reduced Product Combination of Abstract Domains for Shapes, in: Verification, Model Checking and Abstract Interpretation (VMCAI'13), Rome, Italie, LNCS, January 2013, to appear.

    http://hal.inria.fr/hal-00760428
  • 28M. 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.

    http://www.dsi.unive.it/~zanioli/publ/sac2012.pdf

Books or Proceedings Editing

  • 29J. Feret, A. Levchenko (editors)

    Proceedings of the 2nd International Workshop on Static Analysis and Systems Biology (SASB 2011), Electronic Notes in Theoretical Computer Science, Elsevier, June 2012, vol. 284, 137 p.

    http://hal.inria.fr/hal-00722482
  • 30A. Miné, D. Schmidt (editors)

    Proceedings of the 19th International Static Analysis Symposium (SAS 2012), LNCS, Springer, September 2012, vol. 7460, 457 p.

    http://hal.inria.fr/hal-00748287
References in notes
  • 31P. 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.
  • 32P. 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.
  • 33R. Cousot.

    Reasoning about program invariance proof methods, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980, no CRIN-80-P050, 22 p.
  • 34P. 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.
  • 35R. Cousot.

    Proving invariance properties of parallel programs by backward induction, University Paul Verlaine, Metz, France, March 1981, no LRIM-82-02, 38 p.
  • 36R. 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.
  • 37P. 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.
  • 38P. 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.
  • 39P. 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.
  • 40P. Cousot, R. Cousot.

    Bi-inductive structural semantics, in: Information and Computation, 2009, vol. 207, no 2, p. 258–283.
  • 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, p. 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, p. 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, p. 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, p. 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, p. 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, no 46.
  • 48V. 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
  • 49V. 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/
  • 50V. 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/
  • 51V. 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/
  • 52V. Danos, C. Laneve.

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

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

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

    http://hal.inria.fr/hal-00520128, http://hal.inria.fr/hal-00520128
  • 54A. Miné.

    Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs, in: ESOP'11 - 20th European Symposium on Programming, Saarbrücken, Allemagne, G. Barthe (editor), Lecture Notes in Computer Science, Springer, 2011, vol. 6602, p. 398-418. [ DOI : 10.1007/978-3-642-19718-5_21 ]

    http://hal.inria.fr/hal-00648038


previous Previous | up Home