HySAT: An efficient proof engine for bounded model checking of hybrid systems
From MaRDI portal
Publication:883144
Recommendations
Cites work
- scientific article; zbMATH DE number 1670796 (Why is no real title available?)
- scientific article; zbMATH DE number 2186837 (Why is no real title available?)
- scientific article; zbMATH DE number 1263213 (Why is no real title available?)
- scientific article; zbMATH DE number 1303060 (Why is no real title available?)
- scientific article; zbMATH DE number 2085252 (Why is no real title available?)
- scientific article; zbMATH DE number 1903356 (Why is no real title available?)
- scientific article; zbMATH DE number 2090300 (Why is no real title available?)
- scientific article; zbMATH DE number 2090318 (Why is no real title available?)
- scientific article; zbMATH DE number 2102695 (Why is no real title available?)
- scientific article; zbMATH DE number 3022422 (Why is no real title available?)
- A linear-time transformation of linear inequalities into conjunctive normal form
- A machine program for theorem-proving
- An incremental algorithm to check satisfiability for bounded model checking
- Automated Reasoning
- Computing small clause normal forms
- Efficient SAT engines for concise logics: accelerating proof search for zero-one linear constraint systems
- Finding a Useful Subset of Constraints for Analysis in an Infeasible Linear Program
- Identifying Minimally Infeasible Subsystems of Inequalities
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Predicative programming Part I
- Verifying industrial hybrid systems with \textsc{MathSAT}
Cited in
(29)- Generating invariants for non-linear hybrid systems
- Rigorous discretization of hybrid systems using process calculi
- Quantitative Model Checking for a Controller Design
- A design of GPU-based quantitative model checking
- Challenges in Constraint-Based Analysis of Hybrid Systems
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Verifying global start-up for a Möbius ring-oscillator
- SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
- Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
- A bounded model checking technique for discrete-time nonlinear systems
- Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- CEGAR Based Bounded Model Checking of Discrete Time Hybrid Systems
- Improving HyLTL model checking of hybrid systems
- HYST: a source transformation and translation tool for hybrid automaton models
- Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods
- HySAT
- Computing branching distances with quantitative games
- Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
- 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
- Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- SMT-based scenario verification for hybrid systems
- Verification, Model Checking, and Abstract Interpretation
- Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
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)
