Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
type: Item
instance of: scholarly article
title: Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
author: Dario Cattaruzza
author: Alessandro Abate
author: Peter Schrammel
author: Daniel Kroening
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7356971
zbMATH Keywords: safety analysis
zbMATH Keywords: invariant generation
zbMATH Keywords: reachability computation
zbMATH Keywords: LTI models
zbMATH Keywords: dynamical models
zbMATH Keywords: abstract acceleration
zbMATH Keywords: CEGAR
describes a project that uses: HySAT
describes a project that uses: ASTREE
describes a project that uses: C2e2
describes a project that uses: HySon
describes a project that uses: Flow*
describes a project that uses: Aspic
describes a project that uses: HyLAA
describes a project that uses: PHAVer
describes a project that uses: HyTech
describes a project that uses: SpaceEx
describes a project that uses: STRONG
describes a project that uses: CORA
describes a project that uses: Interproc
MaRDI profile type: Publication
full work available at URL: s10817-020-09562-z
OpenAlex ID: W3029256966
cites work: Hybridization methods for the analysis of nonlinear systems
cites work: A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra
cites work: Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>
cites work: Q4414726
cites work: Counterexample-Guided Refinement of Template Polyhedra
cites work: Q4953384
cites work: Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
cites work: Sound Numerical Computations in Abstract Acceleration
cites work: SMT-based scenario verification for hybrid systems
cites work: Q2754081
cites work: Computer Aided Verification
cites work: Template-Based Unbounded Time Verification of Affine Hybrid Automata
cites work: SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
cites work: Hybrid Systems: Computation and Control
cites work: HySAT: An efficient proof engine for bounded model checking of hybrid systems
cites work: δ-Complete Decision Procedures for Satisfiability over the Reals
cites work: Combining Widening and Acceleration in Linear Relation Analysis
cites work: Constraint-Based Approach for Analysis of Hybrid Systems
cites work: HyTech: A model checker for hybrid systems
cites work: Abstract acceleration of general linear loops
cites work: Polynomial-time algorithm for the orbit problem
cites work: Q3222981
cites work: Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration
cites work: Reachability Analysis of Hybrid Systems Using Support Functions
cites work: Q5689624
cites work: Q3813179
cites work: Positivity Problems for Low-Order Linear Recurrence Sequences
cites work: Q5849795
cites work: Applying abstract acceleration to (co-)reachability analysis of reactive programs
DOI: 10.1007/S10817-020-09562-Z
description: scientific article; zbMATH DE number 7356971