Bug Hunting in Linux

Supervisor

Suitable for

Abstract

Model Checkers for concurrent programs have made tremendous progress in the past years. It's time to revisit the Linux Kernel with these methods, and investigate scalability and applicability of automated program analysis in this context. This is an applied project.