Explicit-State model checker
Model checker simbólico
Bounded model checking
Generalização de problemas SAT
SMT: Satisfabilidade “modulo” teorias
Z3 (DE MOURA; BJØRNER, 2008):
(declare-fun p () Bool) (declare-fun q () Bool) (assert (implies p q)) (assert p) (assert (not q)) (check-sat)
Resultado: unsat
(declare-fun p () Bool) (declare-fun q () Bool) (assert (implies p q)) (assert p) (assert q) (check-sat)
Resultado: sat
(declare-const a Int) (declare-const b Int) (assert (= (+ a b) 20)) (assert (= (+ a (* 2 b)) 10)) (check-sat) (get-model)
Resultado: sat
Podemos classificar não-determinismo em dois tipos:
1.to(10).oneOf()
any { A, B }
Simulação simbólica: