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

DOI10.1016/J.JSC.2011.12.051zbMATH Open1286.68092OpenAlexW2083013744MaRDI QIDQ435977FDOQ435977

Bertrand Jeannet, Peter Schrammel

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

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

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)

Cites Work

• Combining Widening and Acceleration in Linear Relation Analysis
• Title not available (Why is that?)
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• A modular static analysis approach to affine loop invariants detection
• Abstract interpretation and application to logic programs
• The algorithmic analysis of hybrid systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Using forward reachability analysis for verification of lossy channel systems
• Automated Technology for Verification and Analysis
• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• Fast Acceleration of Ultimately Periodic Relations
• Monotone data flow analysis frameworks
• Title not available (Why is that?)
• Extending abstract acceleration methods to data-flow programs with numerical inputs
• Grids: A Domain for Analyzing the Distribution of Numerical Values
• Computing the Transitive Closure of a Union of Affine Integer Tuple Relations
• Computing convex hulls with a linear solver
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• The Power of Hybrid Acceleration
• Computer Aided Verification
• Proving safety properties of infinite state systems by compilation into Presburger arithmetic

Cited In (3)

• Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
• Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction
• Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration

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)