Generating invariants for non-linear hybrid systems

DOI10.1016/j.tcs.2015.06.018zbMath1328.68130OpenAlexW575850752MaRDI QIDQ2355695

Nadir Matringe, Rachid Rebiha, Arnaldo Vieira Moura

Publication date: 24 July 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2015.06.018

zbMATH Keywords

hybrid systemsformal methodslinear algebrainductive invariant generation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Linear equations (linear algebraic aspects) (15A06)

Related Items (3)

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Pegasus: sound continuous invariant generation ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants

Uses Software

• MetiTarski
• HySAT
• KeYmaera
• HyTech
• Ariadne
• dReal
• ABsolver

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• Quantifier elimination for real algebra -- the quadratic case and beyond
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Constructing invariants for hybrid systems
• Automatic invariant generation for hybrid systems using ideal fixed points
• Automatic abstraction of non-linear systems using change of bases transformations
• Transcendental inductive invariants generation for non-linear differential and hybrid systems
• The Complete Proof Theory of Hybrid Systems
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Constraint-Based Approach for Analysis of Hybrid Systems
• Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization
• Generating Box Invariants
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Applications of MetiTarski in the Verification of Control and Hybrid Systems
• Morphisms for Non-trivial Non-linear Invariant Generation for Algebraic Hybrid Systems
• Abstract interpretation and application to logic programs
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Logical Analysis of Hybrid Systems
• Generating Invariants for Non-linear Hybrid Systems by Linear Algebraic Methods
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Cutting to the Chase Solving Linear Integer Arithmetic
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
• Automated Technology for Verification and Analysis
• Endomorphisms for Non-trivial Non-linear Loop Invariant Generation
• Hybrid Systems: Computation and Control
• Computer Aided Verification

This page was built for publication: Generating invariants for non-linear hybrid systems