[FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF

[Jean Everson Martina]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Quer trazer a discussão In Topic de novo?

Eu falei com o Robert Watson  (FreeBSD Foundation) a umas duas semanas
atras, quando o paper que deu origem a isso tudo foi publicado, e
perguntei quando teríamos uma coisa assim no FreeBSD, e a resposta foi:
"Nunca! Porque a comunidade não tem idéia de quão benéfico isso poderia
ser pro projeto"

Entender e ter condições de discutir este tipo de tópico, é em geral o
que difere um Cientista da Computação de um Micreiro (leia-se prático).

Jean

Paulo Henrique wrote:
> É isso ai lista continuamos a thread... pois a aula está muito
> interessante...
> 
> 2009/10/26 Jean Everson Martina <everson at inf.ufsc.br>
> 
> 
>>>> Um pequeno programa é uma exceção. Algum programa (como esse que você
>>>> falou, talvez), com o espírito acadêmico (principalmente), pode tratar
>>>> exceções. O que não deixa de ter validade empírica, mesmo sabendo da
>>>> existência do Teorema da Parada.
> Você esta confundido a abrangência do teorema de parada. Ele diz que não
> existe algorítimo genérico para decidir a parada para todos os pares
> entrada-programa. O que não quer dizer que não existe solução para casos
> específicos.
> 
> Sobre a validade empírica, você pode explicar o que é uma validade
> formal então?
> 
> De novo, se você estiver correto de que tudo é empírico, um player como
> a MS, não investiria mais de 2 milhões de libras no projeto Terminator
> (o que prova que não é brincadeirinha acadêmica):
> 
> 
> http://research.microsoft.com/en-us/um/cambridge/projects/terminator/default.htm
> 
> O Terminator é um dos maiores responsáveis pelo aumento de estabilidade
> do XP, Vista e 7. Você vê hoje muito menos telas azuis e crashes, porque
> o drivers certificados foram sendo verificados quanto a não parada. Sim,
> se está longe de ter a verificação formal completa de um SO de uso
> genérico. Mas eu digo que em 15 anos isso será um fato.
> 
> Na verdade, tem outros projetos semelhantes sobre verificação de chips
> usando métodos automatizados e logica de ordem mais alta, que são usados
> pela ARM (100% do que a ARM faz é verificado formalmente, e eles são a
> maior plataforma de Micro-processadores hoje). A Intel e AMD também
> fazem mas não em 100% dos casos.
> 
> Aqui mesmo (Grupo de Teoria da Computação de Cambridge), temos projetos
> com a NSA pra verificação formal de micro-processadores criptográficos,
> , com a Cisco e Boeing na área de roteamento, com a IBM na área de
> módulos java e com a Intel na verificação de assembly x86, etc
> 
> Meu PhD é sobre verificação formal de protocolos criptográficos, onde
> parte da pesquisa já foi bancada pela VISA (verificação do SET) e pelo
> Internet Consortium (Verificação do SSL). Hoje o governo brasileiro (que
> me banca) tem interesse em verificar os grandes protocolos no cenário
> nacional, tais como SPB, NF-e e OpenHSM. É por isso que eu to aqui.
> 
> Sobre uma outra pergunta na discussão sobre a usabilidade deste
> microkernel: Sim ele é utilizável e funcional, mas dentro da plataforma
> e objetivos à que se propõe.
> 
> 
> Jean
- -------------------------
Histórico: http://www.fug.com.br/historico/html/freebsd/
Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
>>
> -------------------------
> Histórico: http://www.fug.com.br/historico/html/freebsd/
> Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (Darwin)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkrle+AACgkQQN0Max56WicXnwCgmSgxz/IOiAmyFWIj80QHmNWA
Ez0AnitUbLbgK2CBEs5jmiMfqDbe/rwM
=Lr0k
-----END PGP SIGNATURE-----