HySAT: An efficient proof engine for bounded model checking of hybrid systems
From MaRDI portal
Publication:883144
DOI10.1007/S10703-006-0031-0zbMATH Open1116.68048OpenAlexW2086163366MaRDI QIDQ883144FDOQ883144
Authors: Martin Fränzle, Christian Herde 
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
Recommendations
VerificationHybrid systemsSatisfiabilityBounded model checkingDecision proceduresInfinite-state systems
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Identifying Minimally Infeasible Subsystems of Inequalities
- A machine program for theorem-proving
- A linear-time transformation of linear inequalities into conjunctive normal form
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Computing small clause normal forms
- Title not available (Why is that?)
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Predicative programming Part I
- Finding a Useful Subset of Constraints for Analysis in an Infeasible Linear Program
- Title not available (Why is that?)
- Automated Reasoning
- Title not available (Why is that?)
- Title not available (Why is that?)
- An incremental algorithm to check satisfiability for bounded model checking
- Efficient SAT engines for concise logics: accelerating proof search for zero-one linear constraint systems
Cited In (27)
- SMT-based scenario verification for hybrid systems
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
- Quantitative Model Checking for a Controller Design
- Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems
- Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- A design of GPU-based quantitative model checking
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Rigorous discretization of hybrid systems using process calculi
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Generating invariants for non-linear hybrid systems
- HySAT
- Computing branching distances with quantitative games
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
- Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration
- Verification, Model Checking, and Abstract Interpretation
- Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- Verifying global start-up for a Möbius ring-oscillator
- Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods
- A bounded model checking technique for discrete-time nonlinear systems
- Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
- CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems
Uses Software
This page was built for publication: HySAT: An efficient proof engine for bounded model checking of hybrid systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q883144)
