iSAT
Subproject |
H1/2 |
Categories |
Core algorithms, Model checker / solver for hybrid systems |
Overview |
iSAT is a satisfiability checker for Boolean combinations of potentially non-linear arithmetic constraints over real- and integer-valued variables. The main purpose is bounded model checking of hybrid (discrete-continuous) systems. |
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, iSAT Benchmarks, HySAT Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |