Explicit-State model checker

• Enumera todos os estados
  

• Usa um grafo direcionado com estados e transições (reachability graph) e uma fila de estados para checar
  

• Provavelmente, o tipo de model checker que um de nós escreveria se fôssemos tentar (sem pesquisar um monte antes)
  

Model checker simbólico

• Traduz a especificação para um conjunto de restrições (sem quantificação)
  

• Usa um SMT solver para verificar a satisfabilidade das restrições
  

Bounded model checking

• Necessário definir um número máximo de passos (bound) para o qual gerar restrições. A verificação se dá dentro desse limite, podendo haver estados atingíveis fora desse limite que não satisfazem a propriedade.
  

• Generalização de problemas SAT
  

  • SAT: Problema da satisfabilidade Booleana
    

  • SMT: Satisfabilidade “modulo” teorias
    

    • “modulo” no sentido de “dentro de”
      
    • Permite mais elementos: inteiros, reais, arrays, etc
      

Z3 (DE MOURA; BJØRNER, 2008):

• Leonardo de Moura e Nikolaj Bjørner
  
  • Podcast: Type Theory Forall #33 Z3 and Lean, the Spiritual Journey
    

• Versão em WebAssembly
  
  • https://people.csail.mit.edu/cpitcla/z3.wasm/z3.html
    

(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:

• Não-determinismo de dados (data non-determinism)
  
  • 1.to(10).oneOf()
    

• Não-determinismo de controle (control-flow non-determinism)
  
  • any { A, B }
    

Simulação simbólica:

• Model Checkers: exaustivamente checam todos os dados e fluxos possíveis
  

• Simuladores aleatórios: aleatoriamente checam alguns dados e fluxos
  

• Simulador simbólico: aleatóriamente checa alguns fluxos, mas considerando todos os dados possíveis