Patrick Cousot

Silver Professor; Professor of Computer Science

1972 …2020

Research output per year

If you made any changes in Pure these will be visible here soon.

Research Output

2009

Space software validation using abstract interpretation

Bouissou, O., Conquet, E., Cousot, P., Cousot, R., Feret, J., Ghorbal, K., Goubault, E., Lesens, D., Mauborgne, L., Miné, A., Putot, S., Rival, X. & Turin, M., 2009, Proceedings of DASIA 2009 Conference on DAta Systems In Aerospace. (European Space Agency, (Special Publication) ESA SP; vol. 669 SP).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Why does Astrée scale up?

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A. & Rival, X., Dec 2009, In : Formal Methods in System Design. 35, 3, p. 229-264 36 p.

Research output: Contribution to journalArticle

2010

An abstract domain to discover interval linear equalities

Chen, L., Miné, A., Wang, J. & Cousot, P., 2010, Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. p. 112-128 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5944 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

A Parametric segmentation functor for fully automatic and scalable array content analysis

Cousot, P., Cousot, R. & Logozzo, F., 2010, POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 105-118 14 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

A scalable introduction to formal verification of computer systems by abstract interpretation

Cousot, P. & Cousot, R., 2010, Logics and languages for reliability and security. Esparza, J., Spanfelner, B. & Grumberg, O. (eds.). IOS Press, p. 1-29 (NATO Science for Peace and Security Series D: Information and Communication Security; vol. 25).

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

A scalable segmented decision tree abstract domain

Cousot, P., Cousot, R. & Mauborgne, L., 2010, Time for Verification - Essays in Memory of Amir Pnueli. Manna, Z. & Peled, D. A. (eds.). p. 72-95 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6200 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

ASTREE: Proving the absence of runtime errors

Kastner, D., Wilhelm, S., Nenova, S., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A. & Rival, X., 2010, Embedded real time software and systems (ERTS2 2010), Toulouse, France, May 19-21 2010.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Static analysis and verification of aerospace software by abstract interpretation

Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A. & Rival, X., 2010, AIAA Infotech at Aerospace 2010. American Institute of Aeronautics and Astronautics Inc., 2010-3385. (AIAA Infotech at Aerospace 2010).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Static analysis by abstract interpretation of embedded critical software

Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A. & Rival, X., 2010, Third IEEE International Workshop UML and Formal Methods, Shanghai, China, November 16 2010. IEEE

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2011

A parametric segmentation functor for fully automatic and scalable array content analysis

Cousot, P., Cousot, R. & Logozzo, F., Jan 2011, In : ACM SIGPLAN Notices. 46, 1, p. 105-118 14 p.

Research output: Contribution to journalArticle

Grammar semantics, analysis and parsing by abstract interpretation

Cousot, P. & Cousot, R., Oct 14 2011, In : Theoretical Computer Science. 412, 44, p. 6135-6192 58 p.

Research output: Contribution to journalArticle

L'analyseur statique ASTREE (in French)

Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A. & Rival, X., 2011, Utilisations industrielles des techniques formelles: Interpretation abstraite. Boulanger, J-L. (ed.). Lavoisier, p. 67-114 (Collection IC2, Editions Hermes).

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Linear absolute value relation analysis

Chen, L., Miné, A., Wang, J. & Cousot, P., 2011, Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. p. 156-175 20 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6602 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Logical abstract domains and interpretations

Cousot, P., Cousot, R. & Mauborgne, L., 2011, The Future of Software Engineering. Springer Berlin Heidelberg, p. 48-71 24 p.

Research output: Chapter in Book/Report/Conference proceedingChapter

Precondition inference from intermittent assertions and application to contracts on collections

Cousot, P., Cousot, R. & Logozzo, F., 2011, Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. p. 150-168 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6538 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Static analysis by abstract interpretation of embedded critical software

Bertrane, J., Cousot, P., Feret, J., Mauborgne, L., Mine, A. & Rival, X., Jan 2011, In : ACM SIGSOFT Software Engineering Notes. 36, 1, p. 1-8

Research output: Contribution to journalArticle

The reduced product of abstract domains and the combination of decision procedures

Cousot, P., Cousot, R. & Mauborgne, L., 2011, Foundations of Software Science and Computational Structures - 14th Int. Conf., FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings. p. 456-472 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6604 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2012

An abstract interpretation framework for refactoring with application to extract methods with contracts

Cousot, P., Cousot, R., Logozzo, F. & Barnett, M., Oct 2012, In : ACM SIGPLAN Notices. 47, 10, p. 213-232 20 p.

Research output: Contribution to journalArticle

An abstract interpretation framework for refactoring with application to extract methods with contracts

Cousot, P., Cousot, R., Logozzo, F. & Barnett, M., 2012, SPLASH 2012: OOPSLA'12 - Proceedings of the 2012 ACM International Conference on Object Oriented Programming SystemsLanguages and Applications. p. 213-232 20 p. (Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

An abstract interpretation framework for termination

Cousot, P. & Cousot, R., Jan 2012, In : ACM SIGPLAN Notices. 47, 1, p. 245-257 13 p.

Research output: Contribution to journalArticle

An abstract interpretation framework for termination

Cousot, P. & Cousot, R., 2012, POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 245-257 13 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

A semantic integrated development environment

Logozzo, F., Barnett, M., Fandrich, M., Cousot, P. & Cousot, R., 2012, SPLASH'12 - Proceedings of the 2012 ACM Conference on Systems, Programming, and Applications: Software for Humanity. p. 15-16 2 p. (SPLASH'12 - Proceedings of the 2012 ACM Conference on Systems, Programming, and Applications: Software for Humanity).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Formal verification by abstract interpretation

Cousot, P., 2012, NASA Formal Methods - 4th International Symposium, NFM 2012, Proceedings. p. 3-7 5 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7226 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Probabilistic abstract interpretation

Cousot, P. & Monerau, M., 2012, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. p. 169-193 25 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7211 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Theories, solvers and static analysis by abstract interpretation

Cousot, P., Cousot, R. & Mauborgne, L., Dec 2012, In : Journal of the ACM. 59, 6, 31.

Research output: Contribution to journalArticle

2013

Andromeda: Accurate and scalable security analysis of web applications

Tripp, O., Pistoia, M., Cousot, P., Cousot, R. & Guarnieri, S., 2013, 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, Proceedings. p. 210-225 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7793 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Automatic inference of necessary preconditions

Cousot, P., Cousot, R., Fähndrich, M. & Logozzo, F., 2013, Verification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings. Springer Verlag, p. 128-148 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7737 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2014

Abstract interpretation: Past, present and future

Cousot, P. & Cousot, R., 2014, Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014. Association for Computing Machinery, 2. (Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

A Galois connection calculus for abstract interpretation

Cousot, P. & Cousot, R., 2014, POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 3-4 2 p.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2015

A binary decision tree abstract domain functor

Chen, J. & Cousot, P., 2015, Static Analysis- 22nd International Symposium, SAS 2015, Proceedings. Blazy, S. & Jensen, T. (eds.). Springer Verlag, p. 36-53 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9291).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstracting induction by extrapolation and interpolation

Cousot, P., 2015, Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings. D’Souza, D., Lal, A. & Larsen, K. G. (eds.). Springer Verlag, p. 19-42 24 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8931).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

On Various Abstract Understandings of Abstract Interpretation

Cousot, P., Oct 26 2015, Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015. Institute of Electrical and Electronics Engineers Inc., p. 2-3 2 p. 7307726. (Proceedings - 2015 International Symposium on Theoretical Aspects of Software Engineering, TASE 2015).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Static analysis and verification of aerospace software by abstract interpretation

Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A. & Rival, X., 2015, In : Foundations and Trends in Programming Languages. 2, 2-3, p. 71-190 120 p.

Research output: Contribution to journalArticle

Verification by abstract interpretation, soundness and abstract induction

Cousot, P., Jul 14 2015, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015. Association for Computing Machinery, Inc, p. 1-4 4 p. (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP 2015).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Verification by abstract interpretation, Soundness and abstract induction

Cousot, P., 2015, Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. Falaschi, M. (ed.). Springer Verlag, (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9527).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2017

Finding All Potential Run-Time Errors and Data Races in Automotive Software

Kaestner, D., Miné, A., Schmidt, A., Hille, H., Mauborgne, L., Wilhelm, S., Rival, X., Feret, J., Cousot, P. & Ferdinand, C., Mar 28 2017, In : SAE Technical Papers. 2017-March, March

Research output: Contribution to journalConference article

Ogre and pythia: An invariance proof method for weak consistency models

Alglave, J. & Cousot, P., Jan 1 2017, POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Gordon, A. D. & Castagna, G. (eds.). Association for Computing Machinery, p. 3-18 16 p. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2018

Program analysis is harder than verification: A computability perspective

Cousot, P., Giacobazzi, R. & Ranzato, F., 2018, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Weissenbacher, G. & Chockler, H. (eds.). Springer Verlag, p. 75-95 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10982 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2019

Abstract Semantic Dependency

Cousot, P., 2019, Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Chang, B-Y. E. (ed.). Springer, p. 389-410 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11822 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Calculational Design of a Regular Model Checker by Abstract Interpretation

Cousot, P., 2019, Theoretical Aspects of Computing – ICTAC 2019 - 16th International Colloquium, Proceedings. Hierons, R. M. & Mosbah, M. (eds.). Springer, p. 3-21 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11884 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Responsibility Analysis by Abstract Interpretation

Deng, C. & Cousot, P., 2019, Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Chang, B-Y. E. (ed.). Springer, p. 368-388 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11822 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Syntactic and Semantic Soundness of Structural Dataflow Analysis

Cousot, P., 2019, Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Chang, B-Y. E. (ed.). Springer, p. 96-117 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11822 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Verifying Numerical Programs via Iterative Abstract Testing

Yin, B., Chen, L., Liu, J., Wang, J. & Cousot, P., 2019, Static Analysis - 26th International Symposium, SAS 2019, Proceedings. Chang, B-Y. E. (ed.). Springer, p. 247-267 21 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11822 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2020

On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

Cousot, P., 2020, Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019, Revised Selected Papers. Gabbrielli, M. (ed.). Springer, p. 3-18 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12042 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution