Partager via

Position Available: Research Software Developer at MSR Cambridge

  • Article

SLAyer is a software analysis tool that automatically proves properties about the data-structures constructed/modified by concurrent systems-level code.  Terminator is an additional componenet designed to prove termination and liveness properties.  The joint SLAyer/Terminator team is looking for a developer interested in building the first production version of these tools. This position is in Microsoft’s Research division. It will involve a close partnership with Windows Static Driver Verifier team in Redmond, WA. 

This position will include:

  • Developing the internal components within Terminator and SLAyer
  • Integrating Terminator and SLAyer with the Static Driver Verifier product
  • Developing additional infrastructure for future program verification tools

Candidates should have the following technical qualifications:

  • MS. or Ph.D. in Computer Science
  • 2+ years development experience highly desirable (e.g. experience shipping software)
  • Knowledge of algorithms and techniques of program analysis is necessary, at least, from one of the two angles: formal verification or compiler design.
  • 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 abilities and cross-team collaboration skills

To apply or request further details, please contact our Human Resources Department by email: cambhr@microsoft.com Closing date for applications is Friday, 30 November 2007. Microsoft Research is an equal opportunities employer

Comments