Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration

DOI10.1007/s10817-020-09562-zOpenAlexW3029256966MaRDI QIDQ2031413

Alessandro Abate, Daniel Kroening, Dario Cattaruzza, Peter Schrammel

Publication date: 9 June 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-020-09562-z

zbMATH Keywords

invariant generationdynamical modelssafety analysisreachability computationCEGARabstract accelerationLTI models

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Automated and formal synthesis of neural barrier certificates for dynamical models

Uses Software

• HySAT
• PHAVer
• HyTech
• Aspic
• Interproc
• SpaceEx
• ASTREE
• STRONG
• C2e2
• HySon
• Flow*
• HyLAA
• CORA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Applying abstract acceleration to (co-)reachability analysis of reactive programs
• Hybridization methods for the analysis of nonlinear systems
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra
• HyTech: A model checker for hybrid systems
• SMT-based scenario verification for hybrid systems
• Template-Based Unbounded Time Verification of Affine Hybrid Automata
• δ-Complete Decision Procedures for Satisfiability over the Reals
• Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
• Counterexample-Guided Refinement of Template Polyhedra
• Polynomial-time algorithm for the orbit problem
• Constraint-Based Approach for Analysis of Hybrid Systems
• SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
• Combining Widening and Acceleration in Linear Relation Analysis
• Reachability Analysis of Hybrid Systems Using Support Functions
• Sound Numerical Computations in Abstract Acceleration
• Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration
• Hybrid Systems: Computation and Control
• Positivity Problems for Low-Order Linear Recurrence Sequences
• Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>
• Abstract acceleration of general linear loops
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Computer Aided Verification

This page was built for publication: Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration