LFCS Seminar: Thursday, 18 May - Christine Rizkallah
Title: Language based approaches for facilitating software verification
Abstract:
Software verification is essential for building secure systems. Successful projects such as the verified seL4 microkernel and the verified CompCert C compiler have pushed the boundary of what is deemed feasible in our field. However, many critical software components still remain unverified. Verifying such components using the existing brute-force techniques would be infeasible. Instead, my research vision involves creating methods to reduce the cost of verification without compromising on efficiency or trust.
In this talk, I will present our Cogent language and Dargent extension and demonstrate how they achieve this vision within some domains in computer science. For instance, I will demonstrate how functional languages, uniqueness type systems, and certifying compiler techniques dramatically reduce the cost of verifying efficient filesystems. Furthermore, I will summarise how Dargent, a declarative data layout specification language, eased the verification of device drivers.
LFCS Seminar: Thursday, 18 May - Christine Rizkallah
Thu, 18 May, 11.10am
Venue: IF G.03