HySAT-II
Subproject |
H1/2 |
Categories |
Core algorithms, Model checker / solver for hybrid systems |
Overview |
HySAT-II is a satisfiability checker for Boolean combinations of potentially non-linear arithmetic constraints over real- and integer-valued variables. It is able to search optimal satisfying valuations, i.e. solutions which minimize or maximize the value of an arbitrary variable occuring in the input formula. The main purpose of HySAT-II is bounded model checking of hybrid (discrete-continuous) systems. |
M. Fränzle and C. Herde. HySAT: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design, 30:179-198, 2007. M. Fränzle, C. Herde, S. Ratschan, T. Schubert, and T. Teige. Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation -- Special Issue on SAT/CP Integration, 1:209-236, 2007. |
|
ETCS Train System, Elastic Train Control, Aircraft Collision Avoidance Protocol, HySAT Benchmarks, iSAT Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |