Applying abstract acceleration to (co-)reachability analysis of reactive programs

DOI10.1016/J.JSC.2011.12.051MaRDI QIDQ435977zbMATHOpenAlexFDO

Authors Peter Schrammel, Bertrand Jeannet

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

zbMATH Keywords

abstract interpretationaccelerationstatic analysislinear relation analysis

Mathematics Subject Classification ID

Complexity and performance of numerical algorithms (65Y20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Accelerated Data-Flow Analysis
• Acceleration in Convex Data-Flow Analysis
• Abstract acceleration of general linear loops
• Tools and Algorithms for the Construction and Analysis of Systems

Cites work

• scientific article; zbMATH DE number 1638645 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• scientific article; zbMATH DE number 2090855 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• A modular static analysis approach to affine loop invariants detection
• 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.
• Computing convex hulls with a linear solver
• Computing the Transitive Closure of a Union of Affine Integer Tuple Relations
• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Fast acceleration of ultimately periodic relations
• Grids: A Domain for Analyzing the Distribution of Numerical Values
• Hybrid acceleration using real vector automata (extended abstract)
• Monotone data flow analysis frameworks
• Proving safety properties of infinite state systems by compilation into Presburger arithmetic
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• The Power of Hybrid Acceleration
• The algorithmic analysis of hybrid systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Using forward reachability analysis for verification of lossy channel systems

Cited in

(9)

• Accelerated Data-Flow Analysis
• Abstract acceleration of general linear loops
• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration
• Tools and Algorithms for the Construction and Analysis of Systems
• A calculus for modular loop acceleration
• Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration

Describes a project that uses

Uses Software

• FLATA
• Aspic
• LUSTRE
• FAST

This page was built for publication: Applying abstract acceleration to (co-)reachability analysis of reactive programs

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