Lissom, a source level proof carrying code platform

• Author(s): Gomes, João ; Martins, Daniel ; Sousa, Simão Melo de ; Pinto, Jorge Sousa
• Date: 2006
• Persistent ID: http://hdl.handle.net/1822/5717
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Program verification; Proof-carrying code; Security properties
• Document Type: Conference Object
• Language: English

Description

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.