A modular static analysis approach to affine loop invariants detection

DOI10.1016/J.ENTCS.2010.09.002MaRDI QIDQ2814096zbMATH OpenOpenAlexFDO

Authors Corinne Ancourt, Fabien Coelho, François Irigoin

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 interpretationfixed-point computationloop invariant

Mathematics Subject Classification ID

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

Recommendations

• Computing invariants with transformers: experimental scalability and accuracy
• Automatic modular abstractions for linear constraints
• Automatic modular abstractions for template numerical constraints
• Loop Summarization Using Abstract Transformers
• scientific article; zbMATH DE number 2087567

Cites work

• 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
• Finite Differencing of Computable Expressions
• Guided Static Analysis
• scientific article; zbMATH DE number 830853 (Why is no real title available?)
• Program verification as probabilistic inference
• Proving safety properties of infinite state systems by compilation into Presburger arithmetic

Cited in

(12)

• Convergence: integrating termination and abort-freedom
• Using basis dependence distance vectors in the modified Floyd-Warshall algorithm
• Computing invariants with transformers: experimental scalability and accuracy
• 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
• Loop Summarization Using Abstract Transformers
• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
• Convex invariant refinement by control node splitting: a heuristic approach
• Automatic modular abstractions for linear constraints
• Invariant relations for affine loops
• Algebraic program analysis

This page was built for publication: A modular static analysis approach to affine loop invariants detection

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