Microsoft Research Projects of Interest – Verification and Property Checking

Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.

Verification and Property Checking

Boogie is an intermediate verification language that can be used to build program verifiers.

F7 is an enhanced typechecker for the F# programming language. F7 is based on the premise that it should be possible to check various security properties of F# implementation code by typing.

The project End-to-end Security Verification using Refinement Types is concerned with building, verifying, and deploying systems with provable security guarantees using refinement and affine types to verify programs written in a core subset of F#.

Yogi is a research project about software property checking that combines static analysis with testing.