SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata

DOI10.1007/s10703-014-0210-3zbMath1317.68126OpenAlexW2072325940MaRDI QIDQ479819

Lei Bu, Dingbao Xie, Xuandong Li, Jian-hua Zhao

Publication date: 5 December 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-014-0210-3

zbMATH Keywords

linear programmingSATbounded model checkinglinear hybrid automatairreducible infeasible set

Mathematics Subject Classification ID

Linear programming (90C05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• MiniSat
• HySAT
• CPLEX
• PHAVer
• HyTech
• z3
• Sat4j
• RunLim
• MathSAT
• SpaceEx
• BACH

Cites Work

• The algorithmic analysis of hybrid systems
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• What's decidable about hybrid automata?
• SMT-based scenario verification for hybrid systems
• Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Algorithmic analysis of nonlinear hybrid systems
• Theory and Applications of Satisfiability Testing
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Verification, Model Checking, and Abstract Interpretation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata