Microsoft Research Projects of Interest – Model 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.

Model Checking

The Zing project aims at a flexible and scalable systematic state space exploration infrastructure. It uses high-level models that may involve reasoning with rich background universes or combinations of different theories, that arise in various practical applications.

Z3 is a high-performance theorem prover that supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.