Publications of Patrick Cousot (© copyright notice)


1972, 1974, 1975, 1976, 1977, 1978, 1979, 1980, 1981, 1982, 1983, 1984, 1985, 1986, 1987, 1989, 1990, 1991, 1992, 1993, 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, to appear


1972

  • Patrick Cousot. Un analyseur syntaxique pour grammaires hors contexte ascendant sélectif et général. In Congrès AFCET 72, Brochure 1 Grenoble, France, pages 106—130, 6—9 November 1972.   fran\347ais

    1974

  • Patrick Cousot. Définition interprétative et implantation de languages de programmation. Thèse de Docteur Ingénieur en Informatique, Université Joseph Fourier, Grenoble, France, 14 Décembre 1974.   fran\347ais

    1975

  • Patrick Cousot & Radhia Cousot. Vérification statique de la cohérence dynamique des programmes. In Rapport du contrat IRIA SESORI No 75-035, Laboratoire IMAG, University of Grenoble, France. 125 pages. 23 September 1975.   fran\347ais

  • Patrick Cousot & Radhia Cousot. Static Verification of Dynamic Type Properties of Variables. Research Report R.R. 25, Laboratoire IMAG, University of Grenoble, France. 18 pages. November 1975.

    1976

  • Patrick Cousot & Radhia Cousot. Static Determination of Dynamic Properties of Programs. In B. Robinet, editor, Proceedings of the second international symposium on Programming, Paris, France, pages 106—130, April 13-15 1976, Dunod, Paris.

    1977

  • Patrick Cousot & Radhia 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, USA.

  • Patrick Cousot & Radhia Cousot. Static determination of dynamic properties of generalized type unions. In Proceedings of an ACM Conference on Language Design for Reliable Software, D. Wortman (Ed.), March 28-30, 1977, Raleigh, NC, USA. SIGPLAN Notices, Vol. 12, Nb 3, March 1977, pages 77-94, ACM Press, New York, NY, USA.

  • Patrick Cousot & Radhia Cousot. Static determination of dynamic properties of recursive procedures In IFIP Conference on Formal Description of Programming Concepts, E.J. Neuhold, (Ed.), pages 237-277, St-Andrews, N.B., Canada, 1977. North-Holland Publishing Company (1978).

  • Patrick Cousot & Radhia Cousot. Automatic synthesis of optimal invariant assertions: mathematical foundations In Proceedings of the ACM Symposium on Artificial Intelligence & Programming Languages, 1977, Rochester, NY, USA. SIGPLAN Notices, Vol. 12, Nb 8, 15&—17 August 1977, pages 1-12; SIGART Newsletter, No. 64, 15&—17 August 1977, pages 1-12; ACM Press, New York, NY, USA.

  • Patrick Cousot & Radhia Cousot. Towards a universal model for static analysis of programs Unpublished manuscript, Laboratoire IMAG, Université scientifique et médicale de Grenoble, Grenoble, France. January 1977, 90 p.

  • Patrick Cousot. An introduction to a mathematical theory of global program analysis Unpublished manuscript, Laboratoire IMAG, Université scientifique et médicale de Grenoble, Grenoble, France. March 1977, 19 p.

  • Patrick Cousot & Radhia Cousot. Fixed point approach to the approximate semantic analysis of programs Unpublished manuscript, Laboratoire IMAG, Université scientifique et médicale de Grenoble, Grenoble, France. June 1977, 48 p.

  • Patrick Cousot. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. In Research Report R.R. 88, Laboratoire IMAG, University of Grenoble, France. 15 pages. September 1977.

    1978

  • Patrick Cousot & Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 84—97, Tucson, Arizona, 1978. ACM Press, New York, NY, USA.

  • Patrick Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes.
    Thèse És Sciences Mathématiques, Université Joseph Fourier, Grenoble, France, 21 March 1978.   fran\347ais

    1979

  • Patrick Cousot & Radhia Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages pages 269—282, San Antonio, Texas, 1979. ACM Press, New York, U.S.A.

  • Patrick Cousot Analysis of the behavior of dynamic discrete systems, Part I: deterministic systems. Research Report R.R. 161, Laboratoire IMAG, University of Grenoble, France. 34 pages. Janvier 1979.

  • Patrick Cousot & Radhia Cousot. Constructive versions of Tarski's fixed point theorems. In Pacific Journal of Mathematics, Vol. 82, No. 1, 1979, pp. 43—57.

  • Patrick Cousot & Radhia Cousot. A constructive characterization of the lattices of all retractions, pre-closure, quasi-closure and closure operators on a complete lattice. In Portugaliæ Mathematica, Vol. 38, No. 2, 1979, pp. 185—198.

    1980

  • Patrick Cousot & Radhia Cousot. Semantic analysis of communicating sequential processes. Seventh International Colloquium on Automata, Languages and Programming, Noordwijerhout, The Netherlands, 14—18 July 1980, Lecture Notes in Computer Science 85, pages 119—133. © Springer-Verlag, Berlin, Germany, 1980.

  • Patrick Cousot and Radhia Cousot. Reasoning about program invariance proof methods. Research Report CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980, 22p.

    1981

  • Patrick Cousot. Semantic foundations of program analysis. In S.S. Muchnick & N.D. Jones, editors, Program Flow Analysis: Theory and Applications, Ch. 10, pages 303—342, Prentice-Hall, Inc., Englewood Cliffs, New Jersey, U.S.A., 1981.

    1982

  • Patrick Cousot & Radhia Cousot. Induction principles for proving invariance properties of programs. In D. Néel, editor, Tools & Notions for Program Construction: an Advanced Course, pages 75—119. Cambridge University Press, Cambridge, UK, August 1982.

    1983

  • Patrick Cousot. A Hoare-style axiomatization of Burstall's intermittent assertion method for non-deterministic programs
    Research report LRIM-83-04, University Paul Verlaine of Metz, September 1983.
  • Patrick Cousot and Radhia Cousot. “À la Burstall” induction principles for proving inevitability properties of programs. Research Report LRIM-83-08, University Paul Verlaine of Metz, November 1983.

    1984

  • Patrick Cousot & Radhia Cousot. Invariance Proof Methods and Analysis Techniques For Parallel Programs. In A.W. Biermann, G. Guiho & Y. Kodratoff, editors, Automatic Program Construction Techniques, pages 243—271. Macmillan, New York, 1984.

    1985

  • Patrick Cousot & Radhia Cousot. Principe des Méthodes de Preuve de Propriétés d'Invariance et de Fatalité des Programmes Parallèlesfran\347ais (Principle of invariance and inevitability proof methods of concurrent programs.) In « Parallélisme, communication et synchronisation », J.-P. Verjus et G. Roucairol (Eds.), Éditions du CNRS, Paris, pp. 129—149, 1985.

  • Patrick Cousot & Radhia Cousot. “À la Floyd” induction principles for proving inevitability properties of programs.
    In «Algebraic methods in semantics», M. Nivat & J. Reynolds (Eds.), Cambridge University Press, Cambridge, UK, pp. 277—312, December 1985.

    1987

  • Patrick Cousot & Radhia Cousot. Sometime = Always + Recursion Always, On the Equivalence of the Intermittent and Invariant Assertions Methods for Proving Inevitability Properties of Programs. Acta Informatica 24, 1—31 (1987). © Springer.

    1989

  • Patrick Cousot & Radhia Cousot. A language independent proof of the soundness and completeness of generalized Hoare logic. Information and computation 80(2):165—191 (1989).
    © 1989 Elsevier Science B.V. .

    1990

  • Patrick Cousot. Methods and Logics for Proving Programs. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, chapter 15, pages 843—993. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, The Netherlands, 1990.

    1991

  • Patrick Cousot & Radhia Cousot. Relational abstract interpretation of higher-order functional programs (abstract). Actes JTASPEFL'91, Bordeaux, 9-11 octobre 1991, in BIGRE, no 74, pp. 33-36, IRISA, Rennes, France, 1991.

  • Patrick Cousot & Radhia Cousot. Comparison of the Galois connection and widening/narrowing approaches to abstract interpretation (abstract). Actes JTASPEFL'91, Bordeaux, 9-11 octobre 1991, in BIGRE, no 74, pp. 107-110, IRISA, Rennes, France, 1991.

    1992

  • Patrick Cousot & Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2—3):103—179, 1992.

  • Patrick Cousot & Radhia Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511—547, August 1992.

  • Patrick Cousot & Radhia Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, pages 83—94, Albuquerque, New Mexico, January 1992. ACM Press, New York, U.S.A.

  • Patrick Cousot & Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe & M. Wirsing, editors, Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, Leuven, Belgium, 13—17 August 1992, Lecture Notes in Computer Science 631, pages 269—295. © Springer, Berlin, Germany, 1992.

    1993

  • Patrick Cousot & Radhia Cousot. Galois connection based abstract interpretations for strictness analysis. In D. Bjorner, M. Broy, & I.V. Pottosin, editors, Proceedings of the International Conference on Formal Methods in Programming and their Applications, FMPA'93, Academgorodok, Novosibirsk, Russia. Lecture Notes in Computer Science 735, pages 98—127. © Springer, Berlin, Germany, June 28—July 2, 1993.

  • Patrick Cousot & Radhia Cousot. ``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs. Theoret. Comput. Sci., 120 (1993), no. 1, 123—155.

    1994

  • Patrick Cousot & Radhia Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In Proceedings of the 1994 International Conference on Computer Languages, ICCL'94, Toulouse, France, pages 95—112. IEEE Computer Society Press, Los Alamitos, California, U.S.A., May 16—19, 1994.

    1995

  • Patrick Cousot & Radhia Cousot. Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. In Conference Record of FPCA '95 SIGPLAN/SIGARCH/WG2.8 Conference on Functional Programming and Computer Architecture, pages 170—181, La Jolla, California, U.S.A., 25-28 June 1995. ACM Press, New York, U.S.A.

  • Patrick Cousot & Radhia Cousot. Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game Theoretic Form. In Conference on Computer-Aided Verification, 7th International Conference, CAV '95, P. Wolper (Ed.), Liège, Belgium. Lecture Notes in Computer Science 939, pages 293—308. © Springer, Berlin, Germany, July 3—5, 1995.

    1996

  • Patrick Cousot. Abstract Interpretation. In ACM Computing Surveys, 28(2):324—328, June 1996.

  • Patrick Cousot. Program Analysis: The Abstract Interpretation Perspective. ACM Computing Surveys, Vol. 28, No. 4es (Dec. 1996), Pages 165-es., SIGPLAN Notices, Volume 32, 1997, Pages 73-76.

  • Flemming Nielson, Patrick Cousot, Mads Dam, Pierpaolo Degano, Pierre Jouvelot, Alan Mycroft, & Bent Thomsen. Logical and Operational Methods in the Analysis of Programs and Systems. In Analysis and Verification of Multiple-Agent Languages: 5th LOMAPS Workshop, Stockholm, Sweden, June 24-26, 1996, Selected Papers, Lecture Notes in Computer Science 1192, Springer, Berlin, pp. 1—21, 1996.

    1997

  • Patrick Cousot & Radhia Cousot. Parallel Combination of Abstract Interpretation and Model-Based Automatic Analysis of Software In Proceedings of the first ACM Sigplan workshop on Automatic Analysis of Software, AAS'97, R. Cleaveland & D. Jackson (Eds), Paris, France, pages 91—98, 14 January 1997.

  • Patrick Cousot. Types as Abstract Interpretations. Conference Record of the 24th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Paris, France, 15—17 January 1997. ACM Press, New York, U.S.A. pp. 316-331.

  • Patrick Cousot. Design of Semantics by Abstract Interpretation. Mathematical Foundations of Programming Semantics, Thirteenth Annual Conference (MFPS XIII). Carnegie Mellon University, Pittsburgh, Pennsylvania, USA, March 23-26, 1997.

  • Patrick Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Electronic Notes in Theoretical Computer Science, 6 (1997) URL: http://www.elsevier.nl/locate/entcs/volume6.html, 25 pages.

  • Patrick Cousot. Abstract Interpretation Based Static Analysis Parameterized by Semantics. Proceedings of the 4th International Symposium on Static Analysis, SAS'97, Paris, France, 8-10 September 1997, P. van Hentenryck (Ed.), Lecture Notes in Computer Science 1302, © Springer, Berlin, pp. 388—394.

  • Patrick Cousot & Radhia Cousot. Abstract Interpretation of Algebraic Polynomial Systems. In M. Johnson, editor, Proceedings of the Sixth International Conference on Algebraic Methodology and Software Technology, AMAST'97, Sydney, Australia, Lecture Notes in Computer Science 1349, pages 138—154. © Springer, Berlin, Germany, 13—18 December 1997.

    1998

  • Patrick Cousot. The Calculational Design of a Generic Abstract Interpreter. Course notes for the NATO International Summer School 1998 on Calculational System Design. Marktoberdorf, Germany, 28 July—9 august 1998, organized by F.L. Bauer, M. Broy, E.W. Dijkstra, D. Gries, & C.A.R. Hoare.

    1999

  • Patrick Cousot & Radhia Cousot. Refining Model Checking by Abstract Interpretation. Automated Software Engineering Journal, special issue on Automated Software Analysis, 6(1):69—95, 1999.

  • Patrick Cousot. Directions for Research in Approximate Systems Analysis. Computing Surveys' Electronic Symposium on the Theory of Computation. ACM Computing Surveys, Vol. 31, No. 3es, (Sep. 1999).

    2000

  • Patrick Cousot & Radhia Cousot. Temporal Abstract Interpretation. Conference Record of the 27th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Boston, Mass., 19-21 January 2000. ACM Press, New York, U.S.A. pp. 12-25.

  • Patrick Cousot. Interprétation abstraite. Technique et Science Informatique, Vol. 19, Nb 1-2-3. Janvier 2000, Hermès, Paris, France. pp. 155-164.

  • Patrick Cousot. Partial Completeness of Abstract Fixpoint Checking. Proceedings of the Fourth International Symposium on Abstraction, Reformulations and Approximation, SARA'2000, Horseshoe Bay, Texas, USA, Lecture Notes in Artificial Intelligence 1864, pages 1-25. © Springer, Berlin, Germany, 26—29 July 2000.

  • Patrick Cousot. Abstract Interpretation: Achievements and Perspectives. Proceedings of the SSGRR 2000 Computer & eBusiness International Conference, Compact disk paper 224, L'Aquila, Italy, July 31 - August 6 2000. Scuola Superiore G. Reiss Romoli.

  • Patrick Cousot & Radhia Cousot. Abstract Interpretation Based Program Testing. Proceedings of the SSGRR 2000 Computer & eBusiness International Conference, Compact disk paper 248, L'Aquila, Italy, July 31 - August 6 2000. Scuola Superiore G. Reiss Romoli.

    2001

  • Patrick Cousot. Abstract Interpretation Based Formal Methods and Future Challenges. In Informatics, 10 Years Back - 10 Years Ahead, R. Wilhelm (Ed.), Lecture Notes in Computer Science 2000, pp. 138-156, 2001.

  • Patrick Cousot & Radhia Cousot. A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination. In Electronic Notes in Theoretical Computer Science 45, Stephen Brooks & Michael Mislove (Eds), Elsevier Science Publishers, 2001.

  • Patrick Cousot & Radhia Cousot. Compositional Separate Modular Static Analysis of Programs by Abstract Interpretation. In Proceedings of the Second International Conference on Advances in Infrastructure for E-Business, E-Science and E-Education on the Internet, SSGRR 2001 Compact disk, L'Aquila, Roma, Italy, 6&—12 August, 2001.

  • Patrick Cousot & Radhia Cousot. Verification of Embedded Software: Problems and Perspectives. In Proceedings of the First International Workshop on Embedded Software, EMSOFT 2001, October, 8th - 10th, 2001, Tahoe City, California, U.S.A. Thomas A. Henzinger & Christoph M. Kirsch (Eds.), Lecture Notes in Computer Science 2211, pp. 97&—113. © Springer.

  • Patrick Cousot . Design of Syntactic Program Transformations by Abstract Interpretation of Semantic Transformations. In Proceedings of the 17th International Conference, ICLP 2001, Philippe Codognet (Ed.), Lecture Notes in Computer Science 2237, Paphos, Cyprus, November 26 - December 1, 2001, pp. 4&—5, © Springer.

    2002

  • Patrick Cousot & Radhia Cousot. Systematic Design of Program Transformation Frameworks by Abstract Interpretation. In Conference Record of the 29th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002. ACM Press, New York, U.S.A. pp. 178&—190.

  • Patrick Cousot. Abstract Interpretation: Theory and Practice. In Proceedings of the 9th International SPIN Workshop, Grenoble, France, Lecture Notes in Computer Science 2318, Dragan Bosnacki & Stephen Leue (Eds.), Grenoble, France, April 11-13, 2002, pp. 2-5. © Springer

  • Patrick Cousot & Radhia Cousot. Modular Static Program Analysis. In Proceedings of the Eleventh International Conference on Compiler Construction (CC 2002), Grenoble, France, April 6—14, 2002. Lecture Notes in Computer Science 2304, pp. 159&—178, © Springer.

  • Patrick Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Theoretical Computer Science,, 277(1—2):47—103, 2002. © Elsevier Science.

  • Patrick Cousot & Radhia Cousot. On Abstraction in Software Verification. In Proceedings of the 14th International Conference on Computer Aided Verification, CAV 2002, Copenhagen, Denmark, July 2002 Copenhagen, Denmark, 27—31 July 2002. Lecture Notes in Computer Science 2404, pp. 37—56, © Springer.

  • Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival. Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen, D.A. Schmidt & I.H. Sudborough (Editors). Lecture Notes in Computer Science 2566, pp. 85—108, © Springer.

    2003

  • Patrick Cousot & Radhia Cousot. Parsing as Abstract Interpretation of Grammar Semantics. Theoretical Computer Science 290:531-544 (2003). © Elsevier Science.

  • Patrick Cousot. Automatic Verification by Abstract Interpretation. In VMCAI 2003 — Fourth International Conference on Verification, Model Checking and Abstract Interpretation, L.D. Zuck, P.C. Attie, A. Cortesi, & S. Mukhopadhyay (Editors). Lecture Notes in Computer Science 2566, pp. 85—108, © Springer.

  • Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival. A Static Analyzer for Large Safety-Critical Software. In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation , 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196—207, © ACM.

    2004

  • Patrick Cousot & Radhia Cousot. An Abstract Interpretation-Based Framework for Software Watermarking. In Conference Record of the 31st ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Venice, Italy, January 14-16, 2004. ACM Press, New York, U.S.A. pp. 173—185. & copy; ACM.

  • Patrick Cousot. Verification by Abstract Interpretation. In International Symposium on Verification — Theory & Practice — Honoring Zohar Manna's 64th Birthday, Sunday, June 29 — Friday, July 4, 2003, Taormina, Sicily, Italy, Lecture Notes in Computer Science, vol. 2772, Nachum Dershowitz (Ed.), pp. 243—268, © Springer, Berlin.

  • Patrick Cousot & Radhia Cousot. Basic Concepts of Abstract Interpretation. In Building the Information Society , René Jacquard (Ed.), Kluwer Academic Publishers, pp. 359—366, 2004. (IFIP WCC 2004 Toulouse, Topical Day on Abstract Interpretation, Tuesday 24 August 2004).

    2005

  • Patrick Cousot. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, January 17—19, 2005. Lecture Notes in Computer Science 3385, © Springer, Berlin, pp. 1—24.

  • Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, David Monniaux, Laurent Mauborgne, Xavier Rival. The ASTRÉE Analyzer. ESOP 2005: The European Symposium on Programming, Edinburgh, Scotland, April 2—10, 2005. Lecture Notes in Computer Science 3444, © Springer, Berlin, pp. 21—30.

  • Patrick Cousot. The Verification Grand Challenge and Abstract Interpretation. Verified Software: Theories, Tools, Experiments (VSTTE), ETH Zürich, Switzerland, October 10th—13th, 2005.

  • Patrick Cousot. Integrating Physical Systems in the Static Analysis of Embedded Control Software. The Third Asian Symposium on Programming Languages and Systems (APLAS'05), Tsukuba, Japan, November 3—5, 2005. Lecture Notes in Computer Science, volume 3780, © Springer, Berlin, pp. 135—138.

    2006

  • Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux,& Xavier Rival. Combination of Abstractions in the ASTRÉE Static Analyzer. In 11th Annual Asian Computing Science Conference (ASIAN'06), National Center of Sciences, Tokyo, Japan, December 6—8, 2006. LNCS 4435, © Springer-Verlag, pp. 272—300.

  • Patrick Cousot & Radhia Cousot. Grammar Analysis and Parsing by Abstract Interpretation. In Program Analysis and Compilation, Theory and Practice: Essays dedicated to Reinhard Wilhelm, T. Reps, M. Sagiv & J. Bauer (Eds.), Lecture Notes in Computer Science 4444, pp. 178—203, © Springer-Verlag, Berlin, December 2006.

    2007

  • Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival. Varieties of Static Analyzers: A Comparison with ASTRÉE. First IEEE & IFIP International Symposium on ``Theoretical Aspects of Software Engineering'', TASE'07, Shanghai, China, 6—8 June 2007, pp. 3—17.

  • Patrick Cousot, Pierre Ganty, Jean-François Raskin. Fixpoint-Guided Abstraction Refinements. In 14th Fourteenth International Symposium on Static Analysis, (SAS'07), The Technical University of Denmark, Kongens Lyngby, Denmark, August 22—24, 2006. LNCS 4634, © Springer-Verlag, Berlin, pp. 333—348.

  • Patrick Cousot. The Rôle of Abstract Interpretation in Formal Methods. In SEFM 2007, 5th IEEE International Conference on Software Engineering and Formal Methods, Mike Hinchey & Tiziana Margaria (Eds.), London, UK, September 10—14, 2007, IEEE Press, pages 135—137.

  • Patrick Cousot. Proving the Absence of Run-Time Errors in Safety-Critical Avionics Code. In Proceedings of the Seventh ACM & IEEE International Conference on Embedded Software (EMSOFT 2007), Embedded Systems Week, Salzburg, Austria, September 30th—Oct. 3rd, 2007, pp . 7—9, ACM Press.

  • Patrick Cousot & Radhia Cousot. Bi-inductive Structural Semantics. In Structural Operational Semantics 2007, Rob van Glabbeek & Matthew Hennessy (Eds), July 9, 2007, Wroclaw, Poland. ENTCS, Volume 192, Issue 1, 24 October 2007, pp. 29-44, © Elsevier, Amsterdam, The Netherlands.

  • Patrick Cousot. The Verification Grand Challenge and Abstract Interpretation. In Verified Software: Tools, Theories, Experiments, Bertrand Meyer & Jim Woodcock (Eds), LNCS 4171, © Springer-Verlag, Berlin, pp. 227—240, Dec. 2007.

    2008

  • Mike Hinchey, Michael Jackson, Patrick Cousot, Byron Cook, Jonathan P. Bowen, & Tiziana Margaria. Software engineering and formal methods. Commun. ACM 51(9): 54—59 (Sep. 2008).

  • Liqian Chen, Antoine Miné, & Patrick Cousot. A Sound Floating-Point Polyhedra Abstract Domain. In Proc. of the 6th Asian Symposium on Programming Languages and Systems (APLAS 2008), volume 5356 of LNCS, pages 3—18, Springer, Bangalore, India, Dec 9—11, 2008.

    2009

  • Patrick Cousot & Radhia Cousot. Bi-inductive Structural Semantics. In Information and computation 207(2):258—283, February 2009.

  • Olivier Bouissou, Éric Conquet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Khalil Ghorbal, Éric Goubault, David Lesens, Laurent Mauborgne, Antoine Miné, Sylvie Putot, Xavier Rival, & Michel Turin. Space Software Validation using Abstract Interpretation. In Proc. of the Int. Space System Engineering Conf., Data Systems in Aerospace (DASIA 2009). Istambul, Turkey, May 2009, 7 pages. ESA.

  • Daniel Kästner, Christian Ferdinand, Stephan Wilhelm, Stefana Nevona, Olha Honcharova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival, and Élodie-Jane Sims. Astrée: Nachweis der Abwesenheit von Laufzeitfehlern.   (in german) In Workshop ``Entwicklung zuverlässiger Software-Systeme'', Regensburg, Germany, June 18th, 2009.

  • Liqian Chen, Antoine Miné, Ji Wang, & Patrick Cousot. Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships. In Proc. of the 16th International Static Analysis Symposium (SAS'09), volume 5673 of Lecture Notes in Computer Science, pages 309—325, Los Angeles, CA, USA, August 2009.

  • Patrick Cousot, Radhia Cousot, & Roberto Giacobazzi. The abstract interpretation of resolution-based semantics. In Abstract Interpretation and Logic Programming: In honor of professor Giorgio Levi, M. Falaschi, M. Gabbrielli, & C. Palamidessi (Eds), Theoretical Computer Science, Volume 410, Issue 46, 1 November 2009, Pages 4724—4746, Elsevier B.V.

  • P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, & X. Rival. Why does Astrée scale up? In Formal Methods in System Design, Volume 35, Number 3, Pages 229—264. December, 2009.

    2010

  • Liqian Chen, Antoine Miné, Ji Wang, & Patrick Cousot. An Abstract Domain to Discover Interval Linear Equalities. Proc. of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'10), Gilles Barthe, Manuel V. Hermenegildo (Eds.), Lecture Notes in Computer Science 5944, Pages 112—128, © Springer, Madrid, Spain, 17—19 January 2010.

  • Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, & Xavier Rival. Static Analysis and Verification of Aerospace Software by Abstract Interpretation. In AIAA Infotech@@Aerospace 2010, Atlanta, Georgia. American Institute of Aeronautics and Astronautics, 20—22 April 2010. © AIAA.

  • Patrick Cousot, Radhia Cousot, & Laurent Mauborgne. A Scalable Segmented Decision Tree Abstract Domain. In Time for Verification, Essays in Memory of Amir Pnueli, Z. Manna, D. Peled (Eds). Lecture Notes in Computer Science 6200, Pages 72—95, © Springer, May 2010.

  • Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, & Xavier Rival. ASTRÉE: Proving the Absence of Runtime Errors. In Proc. of the Embedded Real Time Software and Systems (ERTS2 2010). Toulouse, France, May 19—21, 2010.

  • P. Cousot & R. Cousot. A gentle introduction to formal verification of computer systems by abstract interpretation. In Logics and Languages for Reliability and Security, J. Esparza, O. Grumberg, & M. Broy (Eds), NATO Science Series III: Computer and Systems Sciences, © IOS Press, 2010, Pages 1—29.

  • Patrick Cousot, Radhia Cousot, & Laurent Mauborgne. Logical Abstract Domains and Interpretations. In The Future of Software Engineering, S. Nanz (Ed.). © Springer 2010, Pages 48—71.

  • Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, & Xavier Rival. Static Analysis by Abstract Interpretation of Embedded Critical Software. In Third IEEE International workshop UML and Formal Methods, 16 November 2010, Shanghai, China, © IEEE.

    2011

  • Patrick Cousot, Radhia Cousot, & Francesco Logozzo. Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, R. Jhala, D. Schmidt (Eds), Austin, TX, USA, January 26—28, 2011. Lecture Notes in Computer Science, Vol. 6538, pp. 150-168, © Springer 2011.

  • Patrick Cousot, Radhia Cousot, & Francesco Logozzo. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. In Conference Record of the 38th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Austin, TX, USA, January 26—28, pp. 105—118, 2011. © ACM Press, New York.

  • Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival. Static Analysis by Abstract Interpretation of Embedded Critical Software. In ACM SIGSOFT Software Engineering Notes 36(1): 1-8 (2011).

  • Patrick Cousot, Radhia Cousot, and Laurent Mauborgne. The reduced product of abstract domains and the combination of decision procedures. In 14th International Conference on Fondations of Software Science and Computation Structures (FoSSaCS 2011), March 26 — April 3, 2011, Saarbrücken, Germany, Martin Hofmann (Ed.), Lecture Notes in Computer Science, Vol. 6604, © Springer 2011, pages 456—472.

  • Liqian Chen, Antoine Miné, Ji Wang, and Patrick Cousot. Linear Absolute Value Relation Analysis. In 20th European Symposium on Programming (ESOP 2011), March 26 - April 3, 2011, Saarbrücken, Germany, Gilles Barthe (Ed.), Lecture Notes in Computer Science, Vol. 6602, pages 156—175, © Springer 2011.

  • J. Bertrane, P. Cousot, R. Cousot and J. Feret, L. Mauborgne, A. Miné, and X. Rival. L'analyseur statique ASTRÉE. In Utilisations industrielles des techniques formelles : interprétation abstraite (J.-L. Boulanger, Ed.), Hermès Science, Paris, France, June 2011 .

  • Patrick Cousot and Radhia Cousot. Grammar semantics, analysis and parsing by abstract interpretation. In Theoretical Computer Science 412(44): 6135-6192 (2011).

    2012

  • Patrick Cousot & Radhia Cousot. An Abstract Interpretation Framework for Termination. In Conference Record of the 39th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, USA, January 25—27, pp. 245—258, 2012. © ACM Press, New York.

  • Patrick Cousot and Michaël Monerau. Probabilistic Abstract Interpretation. In H. Seidel (Ed), 22nd European Symposium on Programming (ESOP 2012), Tallinn, Estonia, 24 March—1 April 2012. Lecture Notes in Computer Science, vol. 7211, pp. 166—190, © Springer, 2012.

  • Patrick Cousot. Formal Verification by Abstract Interpretation. In Alwyn Goodloe and Suzette Person (Eds), 4th NASA Formal Methods Symposium (NFM 2012), Norfolk, Virginia, USA, April 3—5, 2012. Lecture Notes in Computer Science, vol. 7211, pp. 3—7, © Springer, 2012.

  • Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Michael Barnett. An abstract interpretation framework for refactoring with application to extract methods with contracts. In 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21—25, 2012, pp. 213—232, 2012. © ACM Press, New York.

  • Francesco Logozzo, Michael Barnett, Manuel Fähndrich, Patrick Cousot, Radhia Cousot. A semantic integrated development environment. In Conference on Systems, Programming, and Applications: Software for Humanity, SPLASH '12, Tucson, AZ, USA, October 21—25, 2012, pp. 15-—16. © ACM Press, New York.

  • Patrick Cousot, Radhia Cousot, & Laurent Mauborgne. Theories, solvers and static analysis by abstract interpretation. In Journal of the Association for Computing Machinery 59(6), 31 p., 2012. © ACM Press, New York.

    2013

  • Patrick Cousot, Radhia Cousot, Manuel Fähndrich, & Francesco Logozzo. Automatic Inference of Necessary Preconditions. In Roberto Giacobazzi, Josh Berdine, Isabella Mastroeni (Eds), 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Rome, Italy, January 21—22, 2013. Lecture Notes in Computer Science, Vol. 7737, pp. 128—148, © Springer 2013.

  • Omer Tripp, Marco Pistoia, Patrick Cousot, Radhia Cousot, and Salvatore Guarnieri. ANDROMEDA: Accurate and Scalable Security Analysis of Web Applications. In Vittorio Cortellessa, D&accutea;niel Varr&accuteo; (Eds.): Fundamental Approaches to Software Engineering — 16th International Conference, FASE 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16—24, 2013. Proceedings. Lecture Notes in Computer Science 7793, Springer 2013.

    2014

  • Patrick Cousot and Radhia Cousot. A Galois connection calculus for abstract interpretation. In 41st ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 22—24, 2014, pp. 2—3, 2014. © ACM Press, New York.

  • Patrick Cousot and Radhia Cousot. Abstract interpretation: Past, Present, and Future. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS) , July 14—18, 2014, Vienna, Austria.

    2015

  • Patrick Cousot. Abstracting Induction by Extrapolation and Interpolation In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen (Eds), 16th International Conference on Verification, Model Checking, and Abstract Interpretation, Mumbai, India, January 12—14, 2015. Lecture Notes in Computer Science, vol. 8931, pp. 19—42, © Springer 2015.

  • Patrick Cousot. Verification by Abstract Interpretation, Soundness and Abstract Induction. In Elvira Albert and Moreno Falaschi (Eds), 17th International Symposium on Principles and Practice of Declarative Programming (PPDP 2015), Siena, Italy, July 14—16, 2015, © ACM SIGPLAN, 2015.

  • Junjie Chen and Patrick Cousot. A Binary Decision Tree Abstract Domain Functor. In Sandrine Blazy and Thomas Jensen (Eds), 22nd International Symposium on Static Analysis (SAS 2015), Saint Malo, France, September 12—14, 2015. LNCS 9291, pp. 36—53, © Springer, 2015.

  • Patrick Cousot. On Various Abstract Understandings of Abstract Interpretation. In Zhiqiu Huang and Jun Sun (Eds), 9th International Symposium on Theoretical Aspects of Software Engineering, Nanjing, China, September 12—14, 2015. © IEEE Computer Society Press, 2015.

    To appear

  • ... To be completed ...


    Copyright notices: ACM, Elsevier B.V., IOS Press, Springer
    Last modified: Sat Sep 19 08:54:32 EDT 2015