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.