HySAT: An efficient proof engine for bounded model checking of hybrid systems

DOI10.1007/s10703-006-0031-0zbMath1116.68048OpenAlexW2086163366MaRDI QIDQ883144

Christian Herde, Martin Fränzle

Publication date: 31 May 2007

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

Full work available at URL: https://doi.org/10.1007/s10703-006-0031-0

zbMATH Keywords

Hybrid systemsSatisfiabilityVerificationBounded model checkingDecision proceduresInfinite-state systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (21)

Quantitative Model Checking for a Controller Design ⋮ Exact Incremental Analysis of Timed Automata with an SMT-Solver ⋮ Rigorous Discretization of Hybrid Systems Using Process Calculi ⋮ Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space ⋮ Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems ⋮ Computing branching distances with quantitative games ⋮ SMT-based scenario verification for hybrid systems ⋮ SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems ⋮ Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic ⋮ SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata ⋮ Verifying global start-up for a Möbius ring-oscillator ⋮ A design of GPU-based quantitative model checking ⋮ 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 ⋮ HySAT ⋮ Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties ⋮ Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming ⋮ Generating invariants for non-linear hybrid systems

Uses Software

• PBS
• SATIRE
• Chaff
• MathSAT

Cites Work

• A linear-time transformation of linear inequalities into conjunctive normal form
• Predicative programming Part I
• Identifying Minimally Infeasible Subsystems of Inequalities
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Finding a Useful Subset of Constraints for Analysis in an Infeasible Linear Program
• Automated Reasoning
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: HySAT: An efficient proof engine for bounded model checking of hybrid systems