328 citations · 353 across the 8 of their papers we have counts for
8 papers
Ceci n'est pas une pipe: AI systems as semantic abstractions
Jade Alglave, Patrick Cousot
An AI system's output is not the fact or world state it appears to describe, but rather an engineered representation. We propose a semantic framework to describe AI systems, to be…
Calculational Design of Hyperlogics by Abstract Interpretation
Patrick Cousot, Jeffery Wang
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, fixpoi…
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Patrick Cousot
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 abst…
Asynchronous Correspondences Between Hybrid Trajectory Semantics
Patrick Cousot
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…
Responsibility Analysis by Abstract Interpretation
Chaoqiang Deng, Patrick Cousot
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…
Syntax and semantics of the weak consistency model specification language cat
Jade Alglave, Patrick Cousot, Luc Maranget
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…
Syntax and analytic semantics of LISA
Jade ALglave, Patrick Cousot
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://v…
A Static Analyzer for Large Safety-Critical Software
Bruno Blanchet, Patrick Cousot, Radhia Cousot +5
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…