Language theory and mathematical logic provide powerful tools for reasoning about, verifying and generating programs.

Research in formal methods focuses on three main targets: computer-assisted verification of advanced mathematics; trustworthy computing (verification of software security, and synthesis of reliable software); verification of distributed systems.

In this broad area of “formal methods”, The Microsoft Research-Inria Joint Centre pursue the following objectives:

• We extend the scope of formal methods to cover broad areas of modern mathematics. The ambition is to empower mathematicians with new tools, facilitating formal verification of hard mathematical proofs and eventually identification of new mathematical results.
• We address the challenges of distributed environments whose behaviour depends on varied interactions between distinct components. There we develop formal methods for proving “safety” and “liveness” properties of such systems.
• We develop solutions for proving security properties of protocols such as correct use of cryptographic primitives.
• We further conceive tools for automatic synthesis of protocols compliant with pre-specified security properties.
• We automate generation of tests for assessing correctness of programs.