Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Papers of P. Cousot
[go: Go Back, main page]

Publications de Patrick Cousot (© droits d'auteur)
Papers of Patrick Cousot (© copyright notice)

1975, 1976, 1977, 1978, 1979, 1980, 1981, 1982, 1984, 1985, 1986, 1987, 1988, 1989, 1990, 1991, 1992, 1993, 1994, 1995, 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, to appear

1975:

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

  • ... à compléter / more to come ...

    1978:

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

  • ... à compléter / more to come ...

    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 & 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:

  • ... à compléter / more to come ...

    1981:

  • Patrick Cousot. Semantic foundations of program analysis. In S.S. Muchnick and 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.

  • ... à compléter / more to come ...

    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èles. fran\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.
    ‘A la Floyd’ induction principles for proving inevitability properties of programs.
    In «Algebraic methods in semantics», M. Nivat and J. Reynolds (Eds.), Cambridge University Press, Cambridge, UK, pp. 277—312, December 1985.

  • ... à compléter / more to come ...

    1986:

  • ... à compléter / more to come ...

    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.

  • ... à compléter / more to come ...

    1988:

  • ... à compléter / more to come ...

    1989:

  • ... à compléter / more to come ...

    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, invited paper. 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-Verlag, 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-Verlag, 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), invited paper. 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, invited paper. 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-Verlag, 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.

    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, invited paper 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, Invited Address. 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-Verlag, pp. 388—394.

  • Patrick Cousot and 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-Verlag, 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 and C.A.R. Hoare.

    1999:

  • Patrick Cousot and 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 and 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-Verlag, 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 and 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 and Radhia Cousot. A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination. In Electronic Notes in Theoretical Computer Science 45, Stephen Brooks and Michael Mislove (Eds), Elsevier Science Publishers, 2001.

  • Patrick Cousot and 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 and Radhia Cousot. Abstract Interpretation Based 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 and 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 and 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 and Stephen Leue (Eds.), Grenoble, France, April 11-13, 2002, pp. 2-5. © Springer

  • Patrick Cousot and Radhia Cousot.
    Modular Static Program Analysis, invited paper..
    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 and Radhia Cousot.
    On Abstraction in Software Verification, invited paper.
    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, invited chapter.
    In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Lecture Notes in Computer Science 2566, pp. 85—108, © Springer.

    2003:

  • Patrick Cousot and 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, invited tutorial..
    In VMCAI 2003 — Fourth International Conference on Verification, Model Checking and Abstract Interpretation, L.D. Zuck, P.C. Attie, A. Cortesi and 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 (Invited paper).
    In Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, January 17—19, 2005. LNCS 3385, Springer, Berlin, pp. 1—24.

    À paraître / to appear:

  • 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

    ACM copyright notice    Springer-Verlag copyright notice
    Retour à / back to: Exposés / Talks, Index, Institutions, Enseignement / Teaching, Recherche / Research, Services
    Email: cousot@di.ens.fr, cousotp@acm.org
    Dernière mise à jour / Last modified :