Acceleration of the abstract fixpoint computation in numerical program analysis

DOI10.1016/J.JSC.2011.12.050MaRDI QIDQ435974zbMATH OpenOpenAlexFDO

Authors Olivier Bouissou, Yassamine Seladji, Alexandre Chapoutot

Publication date 13 July 2012

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2011.12.050

zbMATH Keywords

acceleration of convergenceabstract numerical domainsfixpointKleene iterationnumerical sequence transformationwidening operator with thresholds

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Acceleration of convergence in numerical analysis (65B99)

Recommendations

• Abstract fixpoint computations with numerical acceleration methods
• Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools
• Computer Aided Verification
• Static Analysis by Policy Iteration on Relational Domains
• Abstract interpretation meets convex optimization

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 2087547 (Why is no real title available?)
• scientific article; zbMATH DE number 3238721 (Why is no real title available?)
• A lattice-theoretical fixpoint theorem and its applications
• Abstract Interpretation Frameworks
• Abstract fixpoint computations with numerical acceleration methods
• Accelerated Data-Flow Analysis
• Combining Widening and Acceleration in Linear Relation Analysis
• Computer Aided Verification
• Computer Aided Verification
• Computing polynomial program invariants
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Extrapolation methods for vector sequences
• Extrapolation methods theory and practice
• Generalizations of aitken's process for accelerating the convergence of sequences
• Generating all polynomial invariants in simple loops
• Guided Static Analysis
• Programming Languages and Systems
• Programming Languages and Systems
• Static Analysis by Policy Iteration on Relational Domains
• Static Analysis of Numerical Algorithms
• Static analysis of finite precision computations
• The Epsilon Algorithm and Operational Formulas of Numerical Analysis
• The octagon abstract domain
• Verification, Model Checking, and Abstract Interpretation
• Widening Polyhedra with Landmarks

Cited in

(9)

• Static Analysis by Policy Iteration on Relational Domains
• Memory-efficient fixpoint computation
• Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case
• Sound Numerical Computations in Abstract Acceleration
• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Fast numerical program analysis with reinforcement learning
• Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
• Abstract fixpoint computations with numerical acceleration methods
• Abstract Semantic Differencing for Numerical Programs

Describes a project that uses

Uses Software

• Apron
• Aspic
• ASTREE
• FAST

This page was built for publication: Acceleration of the abstract fixpoint computation in numerical program analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q435974)