Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-hor...
Main Authors: | Cattaruzza, D, Abate, A, Schrammel, P, Kroening, D |
---|---|
Format: | Journal article |
Language: | English |
Published: |
Springer Verlag
2020
|
Similar Items
-
Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
by: Cattaruzza, D, et al.
Published: (2015) -
Sound numerical computations in abstract acceleration
by: Cattaruzza, D, et al.
Published: (2017) -
Unbounded Safety Verification for Hardware Using Software Analyzers
by: Mukherjee, R, et al.
Published: (2015) -
Verification and synthesis of linear systems by abstract acceleration
by: Cattaruzza, D
Published: (2018) -
Verification of Boolean Programs with Unbounded Thread Creation
by: Cook, B, et al.
Published: (2007)