Patrick Cousot's publications on abstract interpretation
For bibliographic references, see ai.bib or
DBLP.
2021
Patrick Cousot.
Principles of Abstract Interpretation, MIT Press, 2021 (to appear).
2019
Patrick Cousot, Roberto Giacobazzi and Francesco Ranzato.
A2I: abstract2 interpretation. (Distinguished paper award)
In Proceedings of the ACM on Programming Languages: Volume 3 Issue POPL, Article No. 42,
January 2019, 31 pages.
Cascais, Portugal, January 16—18, 2019. ACM Press.
(proofs, slides)
(Distinguished paper award)
Chaoqiang Deng and Patrick Cousot.
Responsibility Analysis by Abstract Interpretation.
In arXiv:1907.08251.
Patrick Cousot.
On fixpoint/iteration/variant induction principles for proving
total correctness of programs with denotational semantics. (Best paper award.)
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. Revised Selected Papers.
Lecture Notes in Computer Science 12042, pp. 3—18.
Springer. (slides)
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. Lecture Notes in Computer Science 11822, 2019, pp. 96—117.
Springer. (slides)
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. Lecture Notes in Computer Science 11822, 2019, pp. 247—267.
Springer. (slides)
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. Lecture Notes in Computer Science 11822, 2019, pp. 389—410.
Springer. (slides)
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. Lecture Notes in Computer Science 11822, 2019., pp. 368—388,.
Springer. (slides)
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. Lecture Notes in Computer Science 11884, 2019, pp. 3—21.
Springer. (slides)
2018
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, July 14—17, 2018.
Lecture Notes in Computer Science 10982, 2018,
pp. 75—95. Springer.
2017
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, pp. 3—18. ACM Press.
(slides)
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.
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.
2016
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.
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.
(slides)
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.
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 Interpretation1,
Mumbai, India, January 12—14, 2015.
Lecture Notes in Computer Science 8931, 2015, pp. 19—42. Springer.
(slides)
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 Press.
(slides)
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. Lecture Notes in Computer Science 9291, 2015, pp. 36—53.
Springer. (slides)
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.
(slides)
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), pp. 71—190.
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. ACM Press.
(auxiliary materials, slides)
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.
(slides)
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 7737, 2013, pp. 128—148.
Springer.
(slides)
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, 2013, pp. 210—225. Springer.
(slides)
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.
(slides)
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 7211, 2012, pp. 166—190.
Springer.
(slides)
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 7211, 2012, pp. 3—7,
Springer.
(slides)
Patrick Cousot.
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, 2012, pp. 213—232. ACM Press.
(slides)
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.
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.
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 6538, pp. 150-168, 2011. Springer.
(slides)
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.
(slides)
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 6604, 2011, pp. 456—472. Springer.
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 6602, pp. 156—175, 2011. Springer.
Julien Bertrane, Patrick Cousot, Radhia Cousot and Jérôme Feret,
Laurent Mauborgne, Antoine Miné, and Xavier Rival.
L'analyseur statique ASTRÉE.
In
Utilisations industrielles des techniques formelles : interprétation abstraite
(J.-L. Boulanger, Ed.), Paris, France, June 2011. Hermès Science.
Patrick Cousot and Radhia Cousot.
Grammar semantics, analysis and parsing by abstract interpretation.
In
Theoretical Computer Science 412(44): 6135-6192 (2011).
2010
Patrick Cousot, Radhia. Cousot, Jérôme Feret, Lauret Mauborgne, Antoine Miné, & Xavier. Rival.
Why does Astrée scale up?
In Formal Methods in System Design, Volume 35, Number 3, pp. 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.), Madrid, Spain, 17—19 January 2010.
Lecture Notes in Computer Science 5944, pp. 112—128. Springer,
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.
(slides)
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, May 2010, pp. 72—95. Springer. (slides)
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.
Patrick Cousot & Radhia 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, 2010, pp. 1—29, IOS Press,.
Patrick Cousot, Radhia Cousot, & Laurent Mauborgne.
Logical Abstract Domains and Interpretations.
In The Future of Software Engineering, S. Nanz (Ed.), 2010, pp. 48—71.
Springer.
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.
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 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), Los Angeles, CA, USA, August 2009.
Lecture Notes in Computer Science 5673, pp. 309—325.
Springer.
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,
pp. 4724—4746. Elsevier B.V.
(slides)
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), Bangalore, India, Dec 9—11, 2008.
Lecture Notes in Computer Science 5356, pp. 3—18, Springer.
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).
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.
Lecture Notes in Computer Science 4634, , pp. 333—348.
Springer.
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, pp. 135—137.
(slides)
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.
(slides)
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.
(slides)
Patrick Cousot.
The Verification Grand Challenge
and Abstract Interpretation.
In
Verified Software: Tools, Theories, Experiments,
Bertrand Meyer & Jim Woodcock (Eds),
Lecture Notes in Computer Science 4171, Dec. 2007, pp. 227—240.
Springer.
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.
Lecture Notes in Computer Science 4435, pp. 272—300.
Springer.
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, December 2006,
pp. 178—203.
Springer.
2005
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, pp. 21—30.
Springer.
(slides)
Patrick Cousot.
The Verification Grand Challenge and Abstract Interpretation.
Verified Software: Theories, Tools, Experiments (VSTTE), ETH Zürich, Switzerland, October 10th—13th, 2005.
(slides)
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, pp. 135—138.
Springer.
(slides)
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, pp. 1—24.
Springer.
(slides)
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.. pp. 173—185.
ACM Press.
(slides)
Patrick Cousot.
Verification by Abstract Interpretation.
In International
Symposium on Verification — Theory & Practice — Honoring Zohar
Mann's 64th Birthday, Sunday, June 29 — Friday, July 4, 2003,
Taormina, Sicily, Italy,
\Lecture Notes in
Computer Science 2772, Nachum Dershowitz (Ed.), pp. 243—268, Springer.
(slides)
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).
(slides)
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.
(slides)
Patrick Cousot.
Automatic Verification
by Abstract Interpretation (DRAFT), Unpublished notes, Feb 25, 2003.
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 Press.
(slides)
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, pp. 178—190. ACM Press.
(slides)
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. (French version)
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.
(slides)
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.
(slides)
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.
(slides)
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.
(slides)
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, pp. 12—25. ACM Press.
(slides)
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 and Radhia Cousot.
Abstract Testing versus (Abstract) Model Checking.
Model Checking and Program Analysis,
Schloss Ringberg, Tegernsee, Germany, February 20—23, 2000
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, 26—29 July 2000,
pp. 1—25.
Springer.
(slides)
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.
(slides)
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.
(slides)
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).
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.
(corrigendum, slides)
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,
pp. 91—98, 14 January 1997.
(slides)
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.. pp. 316—331.
(slides)
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.
(slides)
Patrick Cousot.
Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation.
Electronic Notes in Theoretical Computer Science, 6 (1997), 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, pp. 388—394.
Springer.
(slides)
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, 13—18 December 1997, Sydney, Australia,
Lecture Notes in Computer Science 1349, pp. 138—154.
Springer.
(slides)
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), pp. 165-es.,
SIGPLAN Notices, Volume 32, 1997, pp. 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.
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, La Jolla, California, U.S.A.
pp. 170—181, 25-28 June 1995. ACM Press.
(slides)
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, July 3—5, 1995,
P. Wolper (Ed.),
Liège, Belgium.
Lecture Notes in Computer Science 939,
pp. 293—308. Springer.
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, May 16—19, 1994.
pp. 95—112. IEEE Computer Society Press,.
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,
pp. 98—127.
Springer, Berlin, Germany, June 28—July 2, 1993.
(slides)
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.
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,
pp. 83—94, Albuquerque, New Mexico, January 1992. ACM Press..
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, 1992,
pp. 269—295. Springer.
(slides)
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.
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, pp. 843—993.
Elsevier Science Publishers B.V. (North-Holland), Amsterdam, The Netherlands, 1990.
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.
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.
1985
Patrick Cousot & Radhia Cousot.
Principe des Méthodes
de Preuve de Propriétés
d'Invariance et de Fatalité des Programmes
Parallèles
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.
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, pp. 243—271. Macmillan,
New York, 1984.
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.
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,
pp. 75—119. Cambridge University Press,
Cambridge, UK, August 1982.
1981
Patrick Cousot.
Semantic foundations of program analysis.
In S.S. Muchnick & N.D. Jones, editors, Program Flow
Analysis: Theory and Applications, Ch. 10, pp. 303—342,
Prentice-Hall, Inc., Englewood Cliffs, New Jersey, U.S.A., 1981.
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,
pp. 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.
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
pp. 269—282, San Antonio, Texas, 1979. ACM Press.
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.
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,
pp. 84—97, Tucson, Arizona,
1978. ACM Press.
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. 
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, , Los Angeles, California, 1977,
pp. 238—252. ACM Press.
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,
pp. 77—94, ACM Press.
(slides)
Patrick Cousot & Radhia Cousot.
Cousot.
Static determination of
dynamic properties of recursive procedures
In IFIP Conference on Formal Description of Programming Concepts,
E.J. Neuhold, (Ed.), pp. 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, pp. 1—12;
SIGART Newsletter, No. 64, 15&—17 August 1977, pp. 1—12;
ACM Press.
(slides)
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.
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,
pp. 106—130, April 13-15 1976, Dunod, Paris.
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.
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.
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.
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,
pp. 106—130, 6—9 November 1972.