Lissom, a Source Level Proof Carrying Code Platform

TL;DR

Lissom is a Proof Carrying Code platform designed to demonstrate the practical application of formal verification tools in real-world environments, engaging students in complex problem-solving.

Contribution

It introduces a PCC architecture aimed at making formal verification accessible and practical for educational and real-world use.

Findings

Interest from students in formal verification tools

Proof of concept for practical PCC implementation

Engagement of students in complex verification tasks

Abstract

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 project.