Propostas de Projectos Práticos - 2007/2008
Esta página apresenta algumas ideias para projectos práticos da disciplina de Lógica Computacional. Os alunos interessados em realizar um projecto devem contactar o docente para definir a atribuição respectiva.
Utilização de SMT Provers na verificação de software
O objectivo deste projecto é o de explorar um
SMT Prover na verificação de software. Um
SMT Prover é uma ferramenta que combina um verificador automático de fórmulas proposicionais com estratégias específicas para lidar com problemas de decisão em teorias específicas (como aritmética linear, manipulação de arrays, etc.). Essas teorias são particularmente orientadas para cobrir as
obrigações de prova resultantes da verificação de programas.
Com este projecto pretende-se validar esse desígnio verificando as obrigações de prova resultantes de programas concretos com um
SMT Prover. Como gerador de obrigações de prova sugere-se a utilização de WHY (
http://why.lri.fr/index.en.html) e como SMT prover o YICES (
http://yices.csl.sri.com/).
Codificação de ORBDDs em Haskell
A codificação de
Binary Decision Diagrams (BDDs) pressupõe um controlo apertado sobre a gestão de memória e nos algoritmos utilizados na sua construção. Esse facto torna a sua codificação em
Haskell um desafio interessante, obrigando à utilização de Monads para permitir aspectos imperativos na sua programação.
Este projecto pretende estudar a implementação de BDDs em Haskell. Tanto pode incidir sobre a codificação "de raiz" dessas estruturas como pode adoptar uma implementação pré-existente a analisar a sua implementação e o respectivo desempenho (e.g. comparando-a com uma biblioteca análoga desenvolvida em C).
Apontadores:
Codificação do algoritmo Davis-Putnam em Haskell
Um dos algoritmos mais utilizados na verificação de fórmulas proposicionais é o
Davis-Putnam(-Logemann-Loveland). Este projecto propõe-se estudar a implementação desse algoritmo em Haskell. Tal como no caso do projecto anterior, o âmbito deste projecto tanto pode incidir sobre a codificação de raiz do algoritmo, como no estudo de uma implementação existente.
Apontadores:
Outros recursos:
Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.