| DATE: | Wed, Feb 8, 2023 |
| TIME: | 11:00 am |
| PLACE: | In SITE 5084 and on Zoom |
| TITLE: | A Language Approach for Facilitating Software Verification |
| PRESENTER: |
Christine Rizkallah
University of Melbourne |
| ABSTRACT:
| |
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 some previous work that achieves this vision within several different areas in computer science. For instance, I will demonstrate how we used functional languages, uniqueness type systems, and certifying compiler techniques to dramatically reduce the cost of verifying efficient filesystems. Furthermore, I will summarise how we used a data layout specification language to ease verifying device drivers.