by Nikolaj Bjorner, Senior Researcher, Microsoft Research
The Research in Software Engineering (RiSE) group at Microsoft Research in Redmond works on several dimensions related to software engineering, including logical foundations, program verification, testing, analysis, empirical software analysis, compiler tools, program optimization, synthesis and model-based software design. This talk describes several of the RiSE groups activities, which are roughly three-pronged: divided between Microsoft product groups, with external developers and with academic interactions.
A significant part of our work involves tool building. The http://rise4fun.com web-site provides an interactive environment where several of the tools developed in RiSE are showcased through interactive demonstrations. I will walk through several of these tools during the talk showing by example our work on graph drawing (AGL), satisfiability modulo theories theorem proving (Z3), program verification (Boogie and VCC), test-case generation using dynamic symbolic execution (Pex), model-based design (FORMULA), symbolic analysis of regular expressions (Rex) and transducers (Bek). I will also describe and present a new tool TouchStudio (http://touchstudioapp.com)
that brings a radically new software development environment to and on the
It is a new programming environment and language built around the new reality of mobile
devices with advanced touchscreens, sensors and cloud connectivity