Lissom, a Source Level Proof Carrying Code Platform
Joao Gomes, Daniel Martins, Simao Melo de Sousa, Jorge Sousa, Pinto

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Advanced Data Storage Technologies · Logic, programming, and type systems
