Extending abstract acceleration methods to data-flow programs with numerical inputs

DOI10.1016/J.ENTCS.2010.09.009MaRDI QIDQ2814110zbMATH OpenOpenAlexFDO

Authors Peter Schrammel, Bertrand Jeannet

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.009

zbMATH Keywords

abstract interpretationaccelerationlinear relation analysisstatic analysis

Mathematics Subject Classification ID

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

Recommendations

• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• Accelerated Data-Flow Analysis
• Acceleration in Convex Data-Flow Analysis
• Sound Numerical Computations in Abstract Acceleration
• Abstract acceleration of general linear loops

Cites work

• Abstract interpretation and application to logic programs
• Automated Technology for Verification and Analysis
• Combining Widening and Acceleration in Linear Relation Analysis
• Computational geometry. Algorithms and applications.
• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• Proving safety properties of infinite state systems by compilation into Presburger arithmetic
• Tools and Algorithms for the Construction and Analysis of Systems
• Using forward reachability analysis for verification of lossy channel systems

Cited in

(8)

• Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
• Accelerated Data-Flow Analysis
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• A calculus for modular loop acceleration
• Sound Numerical Computations in Abstract Acceleration
• Convex invariant refinement by control node splitting: a heuristic approach
• Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration

Describes a project that uses

Uses Software

• LUSTRE
• FAST
• Aspic

This page was built for publication: Extending abstract acceleration methods to data-flow programs with numerical inputs

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