Many aspects of our lives depend critically on software systems. As a result, research on tools, algorithms and methodologies for verifying the correctness of or finding bugs in software has become a hot area from a practical as well as theoretical standpoint. Software verification is the application of mathematical and logic-based techniques to real-life programs. Research in this area builds as much on analytical and mathematical skills as it does on disciplined programming and algorithmic skills.
Our research interests are:
Formal methods for program analysis and verification, automatic static/dynamic program verification, model checking, theorem proving. Design, analysis and verification of concurrent software.
Our missions are:
- To take a holistic, robust approach to the development of novel concurrent programming paradigms and multiprocessor architectures.
- To involve formal methods and verification tool support early in the design process, and to have formal methods, architecture and software systems efforts go hand in hand.
Objectives of the center:
This center combines, for potentially the first time, world-leading researchers in computer architecture, formal methods and systems to produce a coherent, end-to-end, robust methodology for computer architecture design. It leverages existing investments in MSRC, XCG and BSC while bringing in a new key partner at Koc University to strengthen the Microsoft Research capability in this area for future projects.