É isso ai lista continuamos a thread... pois a aula está muito interessante...
2009/10/26 Jean Everson Martina <ever...@inf.ufsc.br> > -----BEGIN PGP SIGNED MESSAGE----- > Hash: SHA1 > > > > 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 > -----BEGIN PGP SIGNATURE----- > Version: GnuPG v1.4.8 (Darwin) > Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ > > iEYEARECAAYFAkrldh0ACgkQQN0Max56Wid4KwCggkNfAxKzj/B5oLBn4Bt1uPty > Ow0AoKbvPMBAmEbKWTe6eQHsN45ULGP8 > =CheR > -----END PGP SIGNATURE----- > ------------------------- > 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
