A Few Graph-Based Relational Numerical Abstract Domains

This article presents the systematic design of a class of relational numerical abstract domains from non-relational ones. Constructed domains represent sets of invariants of the form (vj - vi ? C), where vj and vi are two variables, and C lives in an abstraction of P(Z), P(Q), or P(R). We will call this family of domains weakly relational domains. The underlying concept allowing this construction is an extension of potential graphs and shortest-path closure algorithms in exotic-like algebras.Example constructions are given in order to retrieve well-known domains as well as new ones. Such domains can then be used in the Abstract Interpretation framework in order to design various static analyses. A major benefit of this construction is its modularity, allowing to quickly implement new abstract domains from existing ones.

• Publication year

  2002

• Venue

  Sensors Applications Symposium

• Publication date

  2002-09-17

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/3-540-45789-5_11arXiv cs/0703075
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• An abstract Monte-Carlo method for the analysis of probabilistic programs

  2007cited by this paper
• Modular Static Program Analysis

  2002cited by this paper
• Two Easy Theories Whose Combination is Hard

  2002cited by this paper
• A New Numerical Abstract Domain Based on Difference-Bound Matrices

  2001influential reference
• Cleanness Checking of String Manipulations in C Programs via Integer Analysis

  2001cited by this paper
• The octagon abstract domain

  2001cited by this paper
• Occurrence Counting Analysis for the pi-Calculus

  2000cited by this paper
• A Semantic Basis for Termination Analysis of Logic Programs and its Realization Using Symbolic Norm Constraints

  1997cited by this paper
• E cient Veri cation of Real-Time Systems: Compact Data Structure and State{Space Reduction

  1997cited by this paper
• Static Analyses of Congruence Properties on Rational Numbers (Extended Abstract)

  1997cited by this paper
• Efficient verification of real-time systems: compact data structure and state-space reduction

  1997cited by this paper
• Introduction to algorithms

  1996influential reference
• Interprocedural may-alias analysis for pointers: beyond k-limiting

  1994cited by this paper
• Datalog with Integer Periodicity Constraints

  1994influential reference
• Semantic Analysis of Interval Congruences.

  1993influential reference
• Efficient chaotic iteration strategies with widenings

  1993influential reference
• Abstract Interpretation Frameworks

  1992cited by this paper
• Static Analysis of Linear Congruence Equalities among Variables of a Program

  1991cited by this paper
• Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity

  1990cited by this paper
• Static analysis of arithmetical congruences

  1989cited by this paper
• Deciding Linear Inequalities by Computing Loop Residues

  1981cited by this paper
• Automatic discovery of linear restraints among variables of a program

  1978cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977influential reference
• Static determination of dynamic properties of programs

  1976cited by this paper
• Affine relationships among variables of a program

  1976cited by this paper
• Graphs and Algorithms

  year unknowncited by this paper

• Relational Abstractions Based on Labeled Union-Find

  2025cites this paper
• Universal Synthesis of Differentiably Tunable Numerical Abstract Transformers

  2025cites this paper
• Optimism in Equality Saturation

  2025cites this paper
• Confidence Preservation Property in Knowledge Distillation Abstractions

  2024cites this paper
• Floating-Point TVPI Abstract Domain

  2024cites this paper
• A Fresh Look at Zones and Octagons

  2021cites this paper
• References/Bibliography

  2021cites this paper
• Analysis

  2021cites this paper
• Automatically Tailoring Abstract Interpretation to Custom Usage Scenarios

  2021cites this paper
• Learning fast and precise numerical analysis

  2020cites this paper
• Proving the Absence of Unbounded Polymers in Rule-based Models

  2020cites this paper
• Automatically Tailoring Static Analysis to Custom Usage Scenarios

  2020cites this paper
• Deterministic parallel fixpoint computation

  2019cites this paper
• Reachability Analysis via Orthogonal Sets of Patterns

  2018cites this paper
• The Impact of Program Transformations on Static Program Analysis

  2018cites this paper
• Probabilistic program analysis

  2018cites this paper
• Sound Bit-Precise Numerical Domains

  2017cites this paper
• A practical construction for decomposing numerical abstract domains

  2017cites this paper
• A new abstraction framework for affine transformers

  2017cites this paper
• Two-phase WCET analysis for cache-based symmetric multiprocessor systems

  2017cites this paper
• An Abstract Domain Based on Two-Interval Difference-Bound Matrices

  2016cites this paper
• Automating Abstract Interpretation

  2016cites this paper
• Software Engineering and Methodology for Emerging Domains

  2016influential citation
• A weakly relational domain to detect potential polymerisation events in signaling pathways.

  2015cites this paper
• The SeaHorn Verification Framework

  2015cites this paper
• LLVM bitcode SPACER Z 3-PDR Back End IKOS CEX or Horn ClauseProgram Middle EndFront End

  2015cites this paper
• Sûreté : de l'analyse à l'instrumentation et à la synthèse de code

  2015cites this paper
• Lexical and numerical domains for abstract interpretation

  2013cites this paper
• TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis

  2013cites this paper
• Simplifying the analysis of c++ programs

  2013cites this paper
• The Gauge Domain: Scalable Analysis of Linear Inequality Invariants

  2012cites this paper
• An Introduction to Abstract Interpretation (with a Look at Abstract Fixpoint Checking)

  2012cites this paper
• Abstract Interpretation of Unstructured Imperative Languages on Unbounded Domains

  2011cites this paper
• Automated verification of heap-manipulating programs with infinite data

  2011cites this paper
• One More Step Towards Generalized Graph-Based Weakly Relational Domains

  2011cites this paper
• Static Contract Checking with Abstract Interpretation

  2010cites this paper
• Extending a CP Solver with Congruences as Domains for Program Verification

  2010cites this paper
• Contributions à l'analyse statique de programmes manipulant des tableaux. (Contributions to the Static Analysis of Programs Handling Arrays)

  2010cites this paper
• View-Augmented Abstractions

  2010influential citation
• Automatisation de la Certification Formelle de Systèmes Critiques par Instrumentation d'Interpréteurs Abstraits. (Automatic and formal certification of critical systems by instrumentation of abstract interpreters)

  2010cites this paper
• préparée au laboratoire Vérimag sous la direction de Nicolas Halbwachs dans le cadre de l'École Doctorale Mathématiques, Sciences et Technologies de l'Information, Informatique

  2010cites this paper
• Robust and generic abstract domain for static program analyses : the polyhedral case

  2010cites this paper
• Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness

  2009cites this paper
• Synthèse de gestionnaires mémoire pour applications Java temps-réel embarquées. (Automated memory management for real-time embedded Java applications)

  2008cites this paper
• Pentagons: a weakly relational abstract domain for the efficient validation of array accesses

  2008cites this paper
• Grid domains for analysing software

  2008influential citation
• dans le cadre de l'École Doctorale Mathématiques, Sciences et Technologies de l'Information, Informatique

  2008cites this paper
• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints

  2007cites this paper
• Varieties of Static Analyzers: A Comparison with ASTREE

  2007cites this paper
• Proving the absence of run-time errors in safety-critical avionics code

  2007cites this paper
• Verification of device drivers and intelligent controllers: a case study

  2007cites this paper
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints

  2007cites this paper
• Numeric program analysis techniques with applications to array analysis and library summarization

  2007cites this paper
• Domaines de congruence pour la programmation par contraintes

  2007cites this paper
• The parallel implementation of the Astr´ee static analyzer

  2007cites this paper
• The V3F project

  2006cites this paper
• Grids: A Domain for Analyzing the Distribution of Numerical Values

  2006cites this paper
• Domains with special attention to the congruence domain

  2006cites this paper
• Analyse des systèmes mobiles par interprétation abstraite.

  2005cites this paper
• The Verification Grand Challenge and Abstract Interpretation

  2005cites this paper
• A Linear Domain for Analyzing the Distribution of Numerical Values 1 by

  2005cites this paper
• Verification of an Error Correcting Code by Abstract Interpretation

  2005influential citation
• The Parallel Implementation of the Astrée Static Analyzer

  2005cites this paper
• Widening Operators for Weakly-Relational Numeric Abstractions

  2005cites this paper
• Modular Proof Principles for Parameterised Concretizations

  2005cites this paper
• A framework for numeric analysis of array operations

  2005cites this paper
• Domaines numériques abstraits faiblement relationnels

  2004cites this paper
• Algebraic Power Analysis by Abstract Interpretation

  2004cites this paper
• Weakly Relational Numerical Abstract Domains

  2004cites this paper
• Static Program Analysis via 3-Valued Logic

  2004cites this paper
• Numeric Domains with Summarized Dimensions

  2004cites this paper
• Widening Operators for Weakly-Relational Numeric Abstractions (Extended Abstract)

  2004cites this paper
• Vérification de descriptions VHDL par interprétation abstraite.

  2004cites this paper
• Verification by Abstract Interpretation

  2003cites this paper
• Static Program Analysis via 3-Valued Logic

  2002cites this paper
• Two Variables per Linear Inequality as an Abstract Domain

  2002influential citation
• Numeric Analysis of Array Operations

  year unknowncites this paper
• An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints ?

  year unknowncites this paper