Environment model specifications for more bugs to reveal

Static verification of Linux kernel modules has already helped to reveal hundreds of real bugs in Linux kernel device drivers. On practice software verification tools cannot analyze modules of device drivers with the whole Linux kernel source code. Thus verification of separate modules requires generation of a precise and complete environment model to achieve a suitable false positive rate. I propose to develop a set of specifications for an environment model generator of the LDV Tools system developed in terms of the Linux Driver Verification program. It will help to drastically improve verification results reducing the false positive rate and thus will make it possible to find even more real bugs in the latest versions of the Linux kernel.