Search Results

Documents authored by Cousot, Patrick

Document
DOI: 10.4230/DagRep.6.11.108
Concurrency with Weak Memory Models (Dagstuhl Seminar 16471)

Authors: Jade Alglave, Patrick Cousot, and Caterina Urban

Published in: Dagstuhl Reports, Volume 6, Issue 11 (2017)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 16471 "Concurrency with Weak Memory Models: Semantics, Languages, Compilation, Verification, Static Analysis, and Synthesis". The aim of the seminar was to bring together people from various horizons, including theoreticians and verification practitioners as well as hardware vendors, in order to set up a long-term research program to design formal methods and develop tools ensuring the correctness of concurrent programs on modern multi-processor architectures.
Cite as

Jade Alglave, Patrick Cousot, and Caterina Urban. Concurrency with Weak Memory Models (Dagstuhl Seminar 16471). In Dagstuhl Reports, Volume 6, Issue 11, pp. 108-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{alglave_et_al:DagRep.6.11.108,
  author =	{Alglave, Jade and Cousot, Patrick and Urban, Caterina},
  title =	{{Concurrency with Weak Memory Models (Dagstuhl Seminar 16471)}},
  pages =	{108--128},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{6},
  number =	{11},
  editor =	{Alglave, Jade and Cousot, Patrick and Urban, Caterina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.6.11.108},
  URN =		{urn:nbn:de:0030-drops-70415},
  doi =		{10.4230/DagRep.6.11.108},
  annote =	{Keywords: Compilation, Computer Memory, Concurrency, Memory Barrier, Memory Ordering, Micro-Architecture, Multiprocessor, Out-of-Order Execution, Parallelism, Program Synthesis, Programming Language, Semantics, Static Analysis, Verification, Weak Memory Model}
}
Document
DOI: 10.4230/DagRep.4.8.107
Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)

Authors: Patrick Cousot, Daniel Kroening, and Carsten Sinz

Published in: Dagstuhl Reports, Volume 4, Issue 8 (2015)

Abstract
There has been tremendous progress in static software analysis over the last years with, for example, refined abstract interpretation methods, the advent of fast decision procedures like SAT and SMT solvers, new approaches like software (bounded) model checking or CEGAR, or new problem encodings. We are now close to integrating these techniques into every programmer's toolbox. The aim of the seminar was to bring together developers of software analysis tools and algorithms, including researchers working on the underlying decision procedures (e.g., SMT solvers), and people who are interested in applying these techniques (e.g. in the automotive or avionics industry). The seminar offered the unique chance, by assembling the leading experts in these areas, to make a big step ahead towards new, more powerful tools for static software analysis. Current (academic) tools still suffer from some shortcomings: - Tools are not yet robust enough or support only a subset of a programming language's features. - Scalability to large software packages is not yet sufficient. - There is a lack of standardized property specification and environment modeling constructs, which makes exchange of analysis results more complicated than necessary. - Differing interpretations of programming language semantics by different tools lead to limited trust in analysis results. - Moreover, a comprehensive benchmark collection to compare and evaluate tools is missing. Besides these application-oriented questions, further, more fundamental questions have also been topics of the seminar: - What are the right logics for program verification, bug finding and software analysis? - How can we handle universal quantification? And how to model main memory and complex data structures? - Which decision procedures are most suitable for static software analysis? How can different procedures be combined? Which optimizations to general-purpose decision procedures (SAT/SMT/QBF) are possible in the context of software analysis?
Cite as

Patrick Cousot, Daniel Kroening, and Carsten Sinz. Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352). In Dagstuhl Reports, Volume 4, Issue 8, pp. 107-125, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{cousot_et_al:DagRep.4.8.107,
  author =	{Cousot, Patrick and Kroening, Daniel and Sinz, Carsten},
  title =	{{Next Generation Static Software Analysis Tools (Dagstuhl Seminar 14352)}},
  pages =	{107--125},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{8},
  editor =	{Cousot, Patrick and Kroening, Daniel and Sinz, Carsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.8.107},
  URN =		{urn:nbn:de:0030-drops-48203},
  doi =		{10.4230/DagRep.4.8.107},
  annote =	{Keywords: Software quality, Bug finding, Verification, Decision procedures, SMT/SAT solvers}
}
Document
DOI: 10.4230/DagSemRep.123
Abstract Interpretation (Dagstuhl Seminar 9535)

Authors: Patrick Cousot, Rhadia Cousot, and Alan Mycroft

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Patrick Cousot, Rhadia Cousot, and Alan Mycroft. Abstract Interpretation (Dagstuhl Seminar 9535). Dagstuhl Seminar Report 123, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1995)

Copy BibTex To Clipboard

@TechReport{cousot_et_al:DagSemRep.123,
  author =	{Cousot, Patrick and Cousot, Rhadia and Mycroft, Alan},
  title =	{{Abstract Interpretation (Dagstuhl Seminar 9535)}},
  pages =	{1--20},
  ISSN =	{1619-0203},
  year =	{1995},
  type = 	{Dagstuhl Seminar Report},
  number =	{123},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.123},
  URN =		{urn:nbn:de:0030-drops-150116},
  doi =		{10.4230/DagSemRep.123},
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact