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

DOI10.1007/S10703-014-0210-3MaRDI QIDQ479819zbMATH OpenOpenAlexFDO

Authors Dingbao Xie, Lei Bu, 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

bounded model checkingirreducible infeasible setlinear hybrid automatalinear programmingSAT

Mathematics Subject Classification ID

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

Recommendations

• 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
• Verifying industrial hybrid systems with \textsc{MathSAT}
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• HAT: analyzing linear hybrid automata as labelled transition system

Cites work

• Algorithmic analysis of nonlinear hybrid systems
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1973987 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
• SMT-based scenario verification for hybrid systems
• Symbolic Reachability Analysis of Lazy Linear Hybrid Automata
• The algorithmic analysis of hybrid systems
• Theory and Applications of Satisfiability Testing
• Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
• Verification, Model Checking, and Abstract Interpretation
• Verifying industrial hybrid systems with \textsc{MathSAT}
• What's decidable about hybrid automata?

Cited in

(4)

• 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
• HAT: analyzing linear hybrid automata as labelled transition system

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q479819)