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

DOI10.1016/j.jsc.2011.12.051zbMath1286.68092OpenAlexW2083013744MaRDI QIDQ435977

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

zbMATH Keywords

accelerationstatic analysisabstract interpretationlinear relation analysis

Mathematics Subject Classification ID

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

Related Items (2)

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration

Uses Software

• FLATA
• Aspic
• LUSTRE
• FAST

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
• Monotone data flow analysis frameworks
• Dynamic partitioning in linear relation analysis: application to the verification of reactive systems
• Using forward reachability analysis for verification of lossy channel systems
• A Modular Static Analysis Approach to Affine Loop Invariants Detection
• 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
• Combining Widening and Acceleration in Linear Relation Analysis
• Computing the Transitive Closure of a Union of Affine Integer Tuple Relations
• Abstract interpretation and application to logic programs
• Computing convex hulls with a linear solver
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Technology for Verification and Analysis
• 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

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