Loading...

​​Verificação Formal 2018

​​Mestrado em Engenharia Informática

​​Perfil de Métodos Formais em Engenharia de Software

​​Departamento de Informática, Universidade do Minho

​​​@Jorge S​ 

​​

​​

​​

​​

​​Ferramentas e links relacionados

​​(pela ordem — provável — pela qual serão utilizadas)

​​

​​Uma parte substancial do software listado é desenvolvido em Ocaml, uma linguagem funcional da família ML, e pode ser compilado localmente. Recomenda-se a instalação do package manager OPAM (disponível em Homebrew para Max OSX). 

​​

• ​​SAT Live! - keep up to date with research on the satisfiability problem

• ​​List of SAT solvers

• ​​Recomendado instalar: MiniSat (disponível em Homebrew para Max OSX)

• ​​MiniSat user guide 

• ​​
  

• ​​SMT-LIB - The Satisfiability Modulo Theories Library

• ​​Solvers recomendados:

• ​​Z3 (disponível no Homebrew para Max OSX)

• ​​CVC4 (disponível Cask no Homebrew para Max OSX)

• ​​Yices2 (disponível no Homebrew para Max OSX)

• ​​Alt-ergo (disponível no Opam)

• ​​Documentação (standard e tutorial) 

• ​​
  

• ​​Why3: Where Programs Meet Provers (disponível no Opam)

• ​​versão online

• ​​Docs 

• ​​
  

• ​​The Coq Proof Assistant (disponível no Opam)

• ​​
  

• ​​Frama-C - Software Analyzers (disponível no Opam)

• ​​Docs

• ​​Wiki

• ​​Em particular: 

• ​​ACSL by example

• ​​ACSL Tutorial

​​

• ​​Dafny: A language and program verifier for functional correctness

​​

• ​​CBMC - A Bounded Model Checker for C and C++ programs

• ​​
  

• ​​Máquina virtual com todas as ferramentas instaladas [README], cortesia Maria João Frade:

• ​​Xubuntu-64bit.ova

​​

​​

​​

​​Avaliação