Zobrazeno 1 - 10
of 235
pro vyhledávání: '"COUSOT, PATRICK"'
Autor:
Cousot, Patrick, Wang, Jeffery
Publikováno v:
Proc. ACM Program. Lang. 9, POPL, Article 16 (January 2025), 71 pages
We design various logics for proving hyper properties of iterative programs by application of abstract interpretation principles. In part I, we design a generic, structural, fixpoint abstract interpreter parameterized by an algebraic abstract domain
Externí odkaz:
http://arxiv.org/abs/2411.11113
Autor:
Cousot, Patrick
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural rela
Externí odkaz:
http://arxiv.org/abs/2310.15340
Autor:
Cousot, Patrick
We formalize the semantics of hybrid systems as sets of hybrid trajectories, including those generated by an hybrid transition system. We study the abstraction of hybrid trajectory semantics for verification, static analysis, and refinement. We mainl
Externí odkaz:
http://arxiv.org/abs/2209.14945
Autor:
Deng, Chaoqiang, Cousot, Patrick
Given a behavior of interest in the program, statically determining the corresponding responsible entity is a task of critical importance, especially in program security. Classical static analysis techniques (e.g. dependency analysis, taint analysis,
Externí odkaz:
http://arxiv.org/abs/1907.08251
We provide the syntax and semantics of the cat language, a domain specific language to describe consistency properties of parallel/distributed programs. The language is implemented in the herd7 too (http://diy.inria.fr/doc/herd.html)l.
Externí odkaz:
http://arxiv.org/abs/1608.07531
Autor:
ALglave, Jade, Cousot, Patrick
We provide the syntax and semantics of the LISA (for "Litmus Instruction Set Architecture") language. The parallel assembly language LISA is implemented in the herd7 tool (http://virginia.cs.ucl.ac.uk/herd/) for simulating weak consistency models.
Externí odkaz:
http://arxiv.org/abs/1608.06583
Autor:
Blanchet, Bruno, Cousot, Patrick, Cousot, Radhia, Feret, Jerôme, Mauborgne, Laurent, Miné, Antoine, Monniaux, David, Rival, Xavier
Publikováno v:
PLDI: Conference on Programming Language Design and Implementation (2003) 196 - 207
We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a gener
Externí odkaz:
http://arxiv.org/abs/cs/0701193
Autor:
CHAOQIANG DENG1 deng@cs.nyu.edu, COUSOT, PATRICK1 pcousot@cs.nyu.edu
Publikováno v:
ACM Transactions on Programming Languages & Systems. 2022, Vol. 44 Issue 1, p1-90. 90p.
