Lissom, a source level proof carrying code platform

• Autor(es): Gomes, João ; Martins, Daniel ; Sousa, Simão Melo de ; Pinto, Jorge Sousa
• Data: 2006
• Identificador Persistente: http://hdl.handle.net/1822/5717
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Program verification; Proof-carrying code; Security properties
• Tipo de Documento: Documento de conferência
• Idioma: Inglês

Descrição

This paper introduces a proposal for a Proof Carrying Code (PCC) architecture called Lissom. Started as a challenge for final year Computing students, Lissom was thought as a mean to prove to a sceptic community, and in particular to students, that formal verification tools can be put to practice in a realistic environment, and be used to solve complex and concrete problems. The attractiveness of the problems that PCC addresses has already brought students to show interest in this pro ject.