-
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Authors:
Patrick Cousot
Abstract:
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 compariso…
▽ More
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.
△ Less
Submitted 23 November, 2023; v1 submitted 23 October, 2023;
originally announced October 2023.
-
Asynchronous Correspondences Between Hybrid Trajectory Semantics
Authors:
Patrick Cousot
Abstract:
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…
▽ More
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.
△ Less
Submitted 29 September, 2022;
originally announced September 2022.
-
Responsibility Analysis by Abstract Interpretation
Authors:
Chaoqiang Deng,
Patrick Cousot
Abstract:
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. Mea…
▽ More
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.
△ Less
Submitted 18 July, 2019;
originally announced July 2019.
-
Syntax and semantics of the weak consistency model specification language cat
Authors:
Jade Alglave,
Patrick Cousot,
Luc Maranget
Abstract:
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.
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.
△ Less
Submitted 30 August, 2016; v1 submitted 26 August, 2016;
originally announced August 2016.
-
Syntax and analytic semantics of LISA
Authors:
Jade ALglave,
Patrick Cousot
Abstract:
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.
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.
△ Less
Submitted 23 August, 2016;
originally announced August 2016.
-
A Static Analyzer for Large Safety-Critical Software
Authors:
Bruno Blanchet,
Patrick Cousot,
Radhia Cousot,
Jerôme Feret,
Laurent Mauborgne,
Antoine Miné,
David Monniaux,
Xavier Rival
Abstract:
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…
▽ More
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).
△ Less
Submitted 30 January, 2007;
originally announced January 2007.
