Testador de Teorema Z3 da Microsoft Research

  • Testador de Teorema Z3 da Microsoft Research
 

Testador de Teorema Z3 da Microsoft Research

R$ 25.000,00

Um testador de teorema de alto desempenho que contém solucionadores personalizados para teorias de tipos de dados comuns em teste, verificação, síntese e análise de programas.

Quantidade:

Um testador de teorema de alto desempenho que contém solucionadores personalizados para teorias de tipos de dados comuns em teste, verificação, síntese e análise de programas.

 

 

Descrição Rápida

O Z3 da Microsoft Research é um testador de teorema de alto desempenho que contém vários solucionadores personalizados eficientes para teorias de tipos de dados comuns em teste, verificação, síntese e análise de programas.

O Z3 integra eficientes tecnologias de solução de restrições para satisfabilidade proposicional, funções livres, aritmética linear sobre números reais e inteiros, vetores de bits, tipos de dados algébricos e matrizes aplicadas. Ele pode ser usado para verificar a satisfabilidade de fórmulas lógicas com quantificadores, também utilizando procedimentos de instanciação de qualificadores, saturação e procedimentos de eliminação de quantificadores para números reais, números inteiros e tipos de dados algébricos.

Alem de oferecer suporte a uma ampla base de teorias, o Z3 também é altamente personalizável com uma API extensa e suporte para teorias personalizadas.

  • Testador de teorema de alto desempenho
  • Verifica a satisfabilidade de fórmulas lógicas com quantificadores
  • Inclui suporte para teorias personalizadas
  • Integra eficientes tecnologias de solução de restrições
  • Altamente personalizável com uma API extensa

Requisitos Do Sistema

Processador necessário
2 GHz ou mais rápido
Sistema operacional necessário
Windows 7, Vista ou XP SP3
Memória necessária
1 GB
Espaço em disco necessário
1 GB