System verification

Reducing the costs of verification

Gabriele Keller: 
'Formal verification is time consuming and requires specialist expertise. It's therefore important to autmate as much of the process as possible, so that human proof engineers can focus on the interesting and challenging problems. This is the idea behind the Cogent project, on which we work together with systems and formal methods researchers from Data61/CSIRO in Sydney, Australia, and the University of New South Wales. In close cooperation with the seL4 team, who developed the first fully verified OS micro kernel, we are working on implementing other fully verified systems components, such as file systems and device drivers.