Searcharxiv⌕ Search

arXiv subjects

Patrick Cousot

Publications and source records attributed to Patrick Cousot.

9 recordsLinked to original sources
arXiv2026

Nonstandard Axiomatic Semantics

Similar to Skolem's nonstandard models of Peano's naturals, we show that axiomatic semantics based on Hoare logic has nonstandard models and so does not specify a unique, well-defined, and formal operational semantics of programming languages. We propose to enrich axiomatic semantics with additional proof obligations to solve this ambiguity problem. These proof obligations are always satisfied for standard trace models so that Hoare logic proofs are unchanged for these standard models.

cs.LO↗
arXiv2026

Ceci n'est pas une pipe: AI systems as semantic abstractions

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 able to examine the correctness of such representations. To do so, we distinguish what is justified by accepted domain knowledge, what reference sources say, and what the system can currently use. This allows us to give precise definitions to common failures: extrapolation, refuted or unsupported assertion, sources versus knowledge mismatch, stale or refuted source, added hypotheses, unsupported use... We hope our framework gives a useful vocabulary for specifying and checking AI systems whose outputs, citations, tool calls, and world-changing actions must be justified by reliable claims and explicit authority rather than apparent fluency.

cs.AI↗
arXiv2024

Calculational Design of Hyperlogics by Abstract Interpretation

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 describing finite and infinite computations that can be instantiated for various operational, denotational, or relational program semantics. Considering semantics as program properties, we define a post algebraic transformer for execution properties (e.g. sets of traces) and a Post algebraic transformer for semantic (hyper) properties (e.g. sets of sets of traces), we provide corresponding calculuses as instances of the generic abstract interpreter, and we derive under and over approximation hyperlogics. In part II, we define exact and approximate semantic abstractions, and show that they preserve the mathematical structure of the algebraic semantics, the collecting semantics post, the hyper collecting semantics Post, and the hyperlogics. Since proofs by sound and complete hyperlogics require an exact characterization of the program semantics within the proof, we consider in part III abstractions of the (hyper) semantic properties that yield simplified proof rules. These abstractions include the join, the homomorphic, the elimination, the principal ideal, the order ideal, the frontier order ideal, and the chain limit algebraic abstractions, as well as their combinations, that lead to new algebraic generalizations of hyperlogics, including the \forall\exists^\ast$, $\forall\forall^\ast$, and $\exists\forall-^\ast$ hyperlogics,

cs.LO↗
arXiv2023

Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation

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 relational semantics covering both finite and infinite executions. This understanding of logics as abstractions of a semantics facilitates their comparisons through their respective abstractions of the semantics (rather that the much more difficult comparison through their formal proof systems). More importantly, the formalization provides a calculational method for constructively designing the sound and complete formal proof system by abstraction of the semantics. As an example, we extend Hoare logic to cover all possible behaviors of nondeterministic programs and design a new precondition (in)correctness logic.

cs.LO↗
arXiv2022

Asynchronous Correspondences Between Hybrid Trajectory Semantics

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 mainly consider abstractions of hybrid semantics which establish a correspondence between trajectories derived from a correspondence between states such as homomorphisms, simulations, bisimulations, and preservations with progress. We also consider abstractions that cannot be defined stepwise like discretization. All these abstractions are Galois connections between concrete and abstract hybrid trajectory or discrete trace semantics. In contrast to semantic based abstractions, we investigate the problematic trace-based composition of abstractions.

cs.LO↗
arXiv2019

Responsibility Analysis by Abstract Interpretation

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, slicing, etc.) assist programmers in narrowing down the scope of responsibility, but none of them can explicitly identify the responsible entity. Meanwhile, the causality analysis is generally not pertinent for analyzing programs, and the structural equations model (SEM) of actual causality misses some information inherent in programs, making its analysis on programs imprecise. In this paper, a novel definition of responsibility based on the abstraction of event trace semantics is proposed, which can be applied in program security and other scientific fields. Briefly speaking, an entity ER is responsible for behavior B, if and only if ER is free to choose its input value, and such a choice is the first one that ensures the occurrence of B in the forthcoming execution. Compared to current analysis methods, the responsibility analysis is more precise. In addition, our definition of responsibility takes into account the cognizance of the observer, which, to the best of our knowledge, is a new innovative idea in program analysis.

cs.PL↗
arXiv2016

Syntax and analytic semantics of LISA

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.

cs.PL↗
arXiv2007

A Static Analyzer for Large Safety-Critical Software

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 general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization, the symbolic manipulation of expressions to improve the precision of abstract transfer functions, the octagon, ellipsoid, and decision tree abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds, delayed) and the automatic determination of the parameters (parametrized packing).

cs.PL↗