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,
2016,
2017,
2018,
2019,
2020,
2021,
2022,
2023,
2024,
to appear
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Patrick Cousot & Radhia Cousot.
Principe des Méthodes
de Preuve de Propriétés
d'Invariance et de Fatalité des Programmes
Parallèles.
(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.
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.
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. .
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.
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.
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.
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.
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.
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.
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.
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.sciencedirect.com/science/article/pii/S1571066105801689/pdf?md5=4b5a97e76692842af19bdda646e9dfba&pid=1-s2.0-S1571066105801689-main.pdf, 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.
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.
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).
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.
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.
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.
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.
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).
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.
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.
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.
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.
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 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.
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.
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).
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.
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ániel Varró (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.
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.
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.
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 Foundations and Trends ® in Programming Languages,
Vol. 2, No. 2—3 (2015) 71—190, 2015.
Antoine Miné, Laurent Mauborgne, Xavier Rival, Jérôme Feret, Patrick Cousot,
Daniel Kästner, Stephan Wilhelm, Christian Ferdinand.
Taking Static Analysis to the Next Level:
Proving the Absence of Run-Time Errors and Data Races with Astrée
In 8th European Congress on Embedded Real–Time Software and Systems, Toulouse, 27—29 January 2016, France,
http://www.erts2016.org/programme-thursday.html#th.4.c.
Patrick Cousot.
Construction of invariance proof methods for parallel programs with sequential consistency
In 27th Journées Francophones des Langages,
Jade Alglave and Julien Signoles (Org.), Saint-Malo, France,
January 27-30, 2016. © INRIA, 2016.
Jade Alglave and Patrick Cousot.
Syntax and analytic semantics of LISA
In CoRR, arXiv:1608.06583 [cs.PL],
23 August 2016.
Jade Alglave, Patrick Cousot, and Luc Maranget.
Syntax and semantics of the weak consistency model specification language
cat
In CoRR, arXiv:1608.06583 [cs.PL], 30 August 2016.
Jade Alglave and Patrick Cousot.
Ogre and Pythia, An invariance proof method for weak consistency models.
In Conference Record of the 45th ACM SIGPLAN SIGACT
Symposium on Principles of Programming Languages, Paris, January 18—20, 2017. © ACM Press, New York.
Daniel Kästner, Antoine Miné, Stephan Wilhelm, Xavier Rival,
André Schmidt, Jérôme Feret, Patrick Cousot,
Christian Ferdinand.
Finding All Potential Run-Time Errors and Data Races in Automotive Software
In WCX 17: SAE World Congress Experience,
April 4—6, 2017 Detroit, Michigan, USA,
http://papers.sae.org/2017-01-0054/.
Jade Alglave, Patrick Cousot, and Caterina Urban.
Concurrency with Weak Memory Models.
In Dagstuhl Reports, Schloss Dagstuhl—Leibniz–Zentrum fuer Informatik, Dagstuhl, Germany
Dagstuhl Seminar 16471, Schloss Dagstuhl, Germany,
November 20—25 , 2016.
Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato.
Program Analysis Is Harder Than Verification: A Computability Perspective.
In
Conference on Computer-Aided Verification, 30th International Conference,
CAV '2018,
Oxford, UK. Lecture Notes in Computer Science 10982,
pages 75—95. © Springer-Verlag, Berlin, Germany, July 14—17, 2018.
Patrick Cousot.
A Formal Introduction to Abstract Interpretation.
In
Alexander Pretschner, Peter Müller, and Patrick Stöckle (Eds.):
Engineering Secure and Dependable Software Systems.
NATO Science for Peace and Security, D: Information and Communication Security — Vol. 53
IOS Press, 2019.
Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato.
A2I: abstract2 interpretation.
In Proceedings of the ACM on Programming Languages: Volume 3 Issue POPL, Article No. 42, January 2019, 31 pages. https://doi.org/10.1145/3290355,
Cascais, Portugal, January 16—18, 2019. © ACM Press, New York.
Chaoqiang Deng and Patrick Cousot.
Responsibility Analysis by Abstract Interpretation.
In arXiv:1907.08251arxiv.org/abs/1907.08251.
Patrick Cousot.
On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics
In "Informal pre-proceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019),
Maurizio Gabbrielli (Ed), Porto, Portugal,
October 8-10, 2019. (Best paper award.)
Patrick Cousot.
Syntactic and Semantic Soundness of Structural Dataflow Analysis
In Proceedings of the 26th International Symposium on Static Analysis,
Bor-Yuh Evan Chang (Ed), Porto, Portugal,
October 8-11, 2019. LNCS 11822, pp. 96—117, © Springer, 2019.
Banghu Yin, Liqian Chen, Jiangchao Liu, Ji Wang, and Patrick Cousot.
Verifying Numerical Programs via Iterative Abstract Testing
In Proceedings of the 26th International Symposium on Static Analysis,
Bor-Yuh Evan Chang (Ed), Porto, Portugal,
October 8-11, 2019. LNCS 11822, pp. 247—267, © Springer, 2019.
Patrick Cousot.
Abstract Semantic Dependency
In Proceedings of the 26th International
Symposium on Static Analysis,
Bor-Yuh Evan Chang (Ed), Porto, Portugal,
October 9-11, 2019. LNCS 11822, pp. 389-—410, © Springer, 2019.
Chaoqiang Deng and Patrick Cousot.
Responsibility Analysis by Abstract Interpretation
In Proceedings of the 26th International Symposium on Static Analysis,
Bor-Yuh Evan Chang (Ed), Porto, Portugal,
October 8-11, 2019. LNCS 11822, pp. 368—388, © Springer, 2019.
Patrick Cousot.
Calculational Design of a Regular Model Checker by Abstract Interpretation
In Proceedings of the 16th International Colloquium on Theoretical Aspects
of Computing,
R. M. Hierons and M. Mosbah (Eds.): ICTAC 2019, Hammamet, Tunisia,
October 31—November 4, 2019, Springer LNCS, 2019. LNCS 11884, pp. 3—21, © Springer, 2019.
Patrick Cousot.
Logic in Program Analysis and Verification.
In 2nd Workshop on Logic and Practice of Programming
(LPOP) ,
Nov 15th, 2020. Proceedings (2022), pp. 22-25.
Patrick Cousot.
The Symbolic Term Abstract Domain.
In The 14th International Symposium on Theoretical Aspects of Software Engineering (TASE 2020) ,
December 11-13, 2020, Hangzhou, China.
Patrick Cousot.
Calculational Design of a Regular Model Checker by Abstract Interpretation
Theoretical Computer Science, Volume 869, 12 May 2021, Pages 62-84.
Patrick Cousot.
Program Unrolling by Abstract Interpretation for Probabilistic Proofs.
DARPA SIEVE project, Computer Science, New York University, June 2021.
Patrick Cousot.
Principles of Abstract Interpretation, MIT Press, 21 September 2021.
Patrick Cousot.
Dynamic interval analysis by abstract interpretation.
In 9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2021,
19--29 October 2021, Rhodes, Greece.
Patrick Cousot.
Asynchronous Correspondences Between Hybrid Trajectory Semantics. CoRR abs/2209.14945 (2022)
Chaoqiang Deng and Patrick Cousot.
The Systematic Design of Responsibility Analysis by Abstract Interpretation. ACM Trans. Program. Lang. Syst. 44(1): 3:1-3:90 (2022)
Patrick Cousot.
Asynchronous Correspondences Between Hybrid Trajectory Semantics.
In
J.-F. Raskin and K. Chatterjee (Eds.): Principles of Systems Design, LNCS 13660, Springer, 2023,
Patrick Cousot.
Abstract Interpretation: From 0, 1, To ∞.
In
V. Arceri, A. Cortesi, P. Ferrara, and M. Olliaro (Eds.): Challenges of Software Verification, ISRL 238, Springer Nature Singapore, March 2023,
Patrick Cousot.
Abstract Interpretation of Graphs
Pedro López-García, John P. Gallagher, Roberto Giacobazzi, and (Eds.), Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems. Lecture Notes in Computer Science, vol 13160. Springer, 2023
Patrick Cousot.
The Contributions of Alan Mycroft to Abstract Interpretation
In
Symposium and festschrift to celebrate the work of Prof. Alan Mycroft, 1st December, 2023,
Department of Computer Science and Technology, Cambridge, UK.
Patrick Cousot.
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation.
Proc. ACM Program. Lang. 8, POPL, Article 7, 34 p. (London, UK, January 2024)
Patrick Cousot.
A Personal Historical Perspective on Abstract Interpretation
In The French School of Programming,
Bertrand Meyer (Ed), pp. 205—239, © Springer, 2024.
Patrick Cousot.
On the Design of Program Logics
In Andreas Podelski Festschrift,
15 p., © Springer, 2024.
Copyright notices:
ACM,
Elsevier B.V.,
IOS Press,
Springer