Are you interested in working on cutting edge program analysis tools to find bugs in source code? Do you want to help get rid of those pesky blue screens caused by device drivers? ... The Static Driver Verifier (SDV) and PreFast for Drivers (PFD) teams at Microsoft are looking for an expert in program analysis or formal verification to develop the verification engines of SDV and PFD, and to support rule development. Candidates should have the following technical qualifications:· MS. or Ph.D. in Computer Science· Knowledge of algorithms and techniques of program analysis is necessary, at least, from one of the two angles: formal verification or compiler design. It is expected to be based on college education or, at least 2 years of industrial experience. · Experience with ML-like programming language (F#, OCaml) is highly desirable· Knowledge of and experience with OS internals or driver development is a plus· Good communication and inter-personal skills · Leadership and cross-team collaboration skillsThis position is in the Windows division. It will involve close partnership with Microsoft Research on cutting edge verification technologies. This position will include: · Innovating the verification engines of SDV and PFD, including development of design specifications, implementing new features and responding to customer feature requests· Innovating the rule specification languages of SDV and PFD · Discovering important classes of rules, for example, targeting security bugsSDV and PFD are strategic and high-profile projects within Microsoft. They have the potential to make a critical contribution to the stability of the Windows device drivers and the quality of the device experience of our customers. Full job description .
More info on SDV and PFD can be found via these links: SDV: msdn2.microsoft.com/en-us/library/aa469108.aspxPFD: msdn2.microsoft.com/en-us/library/aa468782.aspx