Combining Widening and Acceleration in Linear Relation Analysis

DOI10.1007/11823230_10MaRDI QIDQ3613383zbMATH OpenOpenAlexFDO

Authors Laure Gonnord, Nicolas Halbwachs

Publication date 12 March 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11823230_10

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Precise widening operators for convex polyhedra
• Acceleration in Convex Data-Flow Analysis
• Abstract fixpoint computations with numerical acceleration methods
• scientific article; zbMATH DE number 2090855
• Accelerated Data-Flow Analysis

Cited in

(24)

• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Descending chains and narrowing on template abstract domains
• Aspic
• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Computing invariants with transformers: experimental scalability and accuracy
• Abstract fixpoint computations with numerical acceleration methods
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Lower runtime bounds for integer programs
• Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
• Improving strategies via SMT solving
• Accelerated Data-Flow Analysis
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• Tree dimension in verification of constrained Horn clauses
• A calculus for modular loop acceleration
• Proving termination by policy iteration
• Convex invariant refinement by control node splitting: a heuristic approach
• Narrowing operators on template abstract domains
• Acceleration in Convex Data-Flow Analysis
• Decoupling the ascending and descending phases in abstract interpretation
• Invariant relations for affine loops
• Poles-based invariant generation for verifying the BIBO stability of digital filters
• Canonical forms and widening for two variables per inequality systems
• Algebraic program analysis

Describes a project that uses

Uses Software

• HyTech

This page was built for publication: Combining Widening and Acceleration in Linear Relation Analysis

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