I am a member of the RiSe (Research in Software Engineering) group. I am working on the SLAM project for checking that software satisfies critical properties of the interfaces it uses. SLAM is a part of the SDV tool that is a static analysis tool for Windows drivers, recently released in Vista WDK (Driver Development Kit) as SDV 1.4. I also developed SDV properties for the new model for driver development KMDF, which is also a part of Vista WDK. SDV 1.5, which supports KMDF drivers, will soon be available as a part of Longhorn Server WDK.