Super interessante artigo, Adolfo! Obrigada pelo link, Valeria 2009/10/26 Adolfo Neto <[email protected]>
> NICTA today announced the completion of the world’s first formal > machine-checked proof of a general-purpose operating system kernel, > promising safety-critical software of unprecedented levels of reliability. > > There is now a way to mathematically prove that the software governing > critical safety and security systems in aircraft and motor vehicles is free > of a large class of errors – long before the plane takes off or the car’s > engine starts. > > The Secure Embedded L4 (seL4) microkernel, designed for real-world use, has > potential applications in defence and other safety and security industries > where the flawless operation of complex embedded systems is of critical > importance. > > “It is hard to comment on this achievement without resorting to clichés,” > says Professor of Computational Logic at Cambridge University’s Computer > Laboratory, Lawrence C Paulson. “Proving the correctness of 7,500 lines of C > code in an operating system's kernel is a unique achievement, which should > eventually lead to software that meets currently unimaginable standards of > reliability.” > > “Formal proofs for specific properties have been conducted for smaller > kernels, but what we have done is a general, functional correctness proof > which has never before been achieved for real-world, high-performance > software of this complexity or size,” explains NICTA Principal Researcher Dr > Gerwin Klein, who leads NICTA’s formal verification research team. > > (...) > > Leia mais em > > http://bit.ly/D2Ghf > > ou, resumido em português, em > > > http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-pronto&id=010150091020&ebol=sim > > > ========================================== > Adolfo Neto > Departamento Acadêmico de Informática > Universidade Tecnológica Federal do Paraná > Fone: (41) 3310-4644 / Fax: (41) 3310-4646 > Web: > http://www.dainf.ct.utfpr.edu.br/~adolfo<http://www.dainf.ct.utfpr.edu.br/%7Eadolfo> > Blog: http://professoradolfo.blogspot.com > ========================================== > > > _______________________________________________ > Logica-l mailing list > [email protected] > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/www/
_______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
