Publications 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, 1996, 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 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.

  • ... ... To be completed ... ...

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

  • ... ... To be completed ... ...

    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

    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.

  • ... ... To be completed ... ...

    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.

  • ... ... To be completed ... ...

    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 & J. Reynolds (Eds.), Cambridge University Press, Cambridge, UK, pp. 277—312, December 1985.

  • ... ... To be completed ... ...

    1986

  • ... ... To be completed ... ...

    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.

  • ... ... To be completed ... ...

    1988

  • ... ... To be completed ... ...

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

  • ... ... To be completed ... ...

    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.

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

    2010

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

    To appear

  • P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, & X. Rival.
    Why does Astrée scale up?
    To appear in Formal Methods in System Design. © Springer. 45 pages.

  • P. Cousot & R. Cousot
    A gentle introduction to formal verification of computer systems by abstract interpretation.
    To appear 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, 29 pages.

  • ... To be completed ...

    Copyright notices: ACM, Elsevier B.V., IOS Press, Springer
    Last modified: Tuesday, 05-Jan-2010 11:24:32 CET