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
  

Às vezes, podemos provar uma invariante qualquer \(I\) (também conhecida como invariante ordinária) mostrando que uma invariante indutiva \(Inv\) implica nela (\(Inv => I\)). Para isso, verificamos três coisas:

1. \(Init => Inv\), ou seja, verificar a propriedade \(Inv\) com --max-steps=0 e garantir que \(Inv\) é verdade em todos os estados iniciais
   
2. \(Inv \land Next => Inv'\), ou seja, verificar a propriedade \(Inv\) a partir de um estado inicial que satisfaça \(Inv\), fazendo um passo (--max-steps=1)
   
3. \(Inv => I\), ou seja, verificar a propriedade \(I\) em todos os estados onde \(Inv\) é verdade (--max-steps=0).
   

Invariância indutiva é muito poderosa porque conseguimos uma prova completa mesmo em model-checking limitado.