LFCS Seminar: Thursday, 18 May - Christine Rizkallah


Title:              Language based approaches for facilitating software verification



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.


May 18 2023 -

LFCS Seminar: Thursday, 18 May - Christine Rizkallah

Christine Rizkallah The University of Melbourne https://people.eng.unimelb.edu.au/rizkallahc/

Thu, 18 May, 11.10am
Venue: IF G.03