SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems

DOI10.1007/978-3-540-88387-6_14zbMath1183.68369OpenAlexW2124397961MaRDI QIDQ3540072

Martin Fränzle, Andreas Eggers, Christian Herde

Publication date: 20 November 2008

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-88387-6_14

Mathematics Subject Classification ID

Interval and finite arithmetic (65G30) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Temporal Logic Verification for Delay Differential Equations ⋮ Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ A CSP versus a zonotope-based method for solving guard set intersection in nonlinear hybrid reachability ⋮ Quantifier-free encoding of invariants for hybrid systems ⋮ Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques ⋮ Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems ⋮ Engineering constraint solvers for automatic analysis of probabilistic hybrid automata ⋮ Challenges in Constraint-Based Analysis of Hybrid Systems ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration ⋮ Monitoring bounded LTL properties using interval analysis ⋮ Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods ⋮ Risk-averse autonomous systems: a brief history and recent developments from the perspective of optimal control

Uses Software

• HySAT
• MathSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Hybrid systems: computation and control. 7th international workshop, HSCC 2004, Philadelphia, PA, USA, March 25--27, 2004. Proceedings.
• Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• A machine program for theorem-proving