Início Theorem-Prover no InfoQ Brasil
Notícias
Feed RSS-
LINQ para Z3, O Mais Rápido Comprovador de Teoremas do Mundo
A Microsoft Research afirma que o Z3 é o mais rápido comprovador de teoremas do mundo. Z3 está projetado para ser uma ferramenta de baixo nível para outras aplicações. Ele é usado por inúmeros projetos incluindo Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, e HAVOC. Com o LINQ criado por Bart De Smet, usar esta ferramenta tornou-se fácil.