A Modular Static Analysis Approach to Affine Loop Invariants Detection

DOI10.1016/j.entcs.2010.09.002zbMath1342.68065OpenAlexW1969311876MaRDI QIDQ2814096

Fabien Coelho, François Irigoin, Corinne Ancourt

Publication date: 17 June 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2010.09.002

zbMATH Keywords

abstract interpretationloop invariantfixed-point computation

Mathematics Subject Classification ID

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

Related Items (8)

Computing invariants with transformers: experimental scalability and accuracy ⋮ Algebraic program analysis ⋮ Convergence: integrating termination and abort-freedom ⋮ Applying abstract acceleration to (co-)reachability analysis of reactive programs ⋮ Convex Invariant Refinement by Control Node Splitting: a Heuristic Approach ⋮ A Modular Static Analysis Approach to Affine Loop Invariants Detection ⋮ Using Basis Dependence Distance Vectors to Calculate the Transitive Closure of Dependence Relations by Means of the Floyd-Warshall Algorithm ⋮ Using basis dependence distance vectors in the modified Floyd-Warshall algorithm

Cites Work

• Unnamed Item
• A calculus of durations
• A Modular Static Analysis Approach to Affine Loop Invariants Detection
• Calculating Exact Transitive Closure for a Normalized Affine Integer Tuple Relation
• Program verification as probabilistic inference
• Guided Static Analysis
• Finite Differencing of Computable Expressions
• Proving safety properties of infinite state systems by compilation into Presburger arithmetic

This page was built for publication: A Modular Static Analysis Approach to Affine Loop Invariants Detection