非线性混合动力系统的有界模型检验

hydlogic translates a reachability problem of a nonlinear hybrid system into a predicate logic formula involving arithmetic constraints, and checks the satisfiability of the formula using a satisfiability modulo theories (SMT) method. We tightly integrate (i) an interval-based solver for hybrid constraint systems (HCSs) to solve the constraints described in the formulas and (ii) an incremental SAT solver to enumerate the possible sets of constraints. The HCS solver verifies an occurrence of a discrete change by enclosing continuous states that may cause the discrete change by a set of boxes.

hydlogic
config
dpllSolver.ml
elisa
examples
formula.ml
ha.ml
ha2smt.ml
hcsPropag.ml
hdlConfig.ml
hdlUtil.ml
hydlogic.sh
incSolver.ml
main.ml
OMakefile
OMakeroot
README
smt.ml
test.ml