Christine received her PhD in 2015 and Kurt was her advisor. She and Kurt worked together with researchers in Wolfgang Paul's and Tobias Nipow's group on verifying algorithmic software.

She is now Senior Lecturer at the University of Melbourne.

https://people.eng.unimelb.edu.au/rizkallahc/

AG 1, INET, AG 5, RG1, SWS, AG 2, AG 4, D6, AG 3   Info

MPI Audience

English

45 Minutes

Saarbrücken

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.

Kurt Mehlhorn

+49 681 9325 1025

--email hidden