Research Software Design Engineer
Office: (425) 707-9705
Fax: (425) 936-7329
Mail: One Microsoft Way, Redmond, WA 98052
I am a member of the RiSe (Research in Software Engineering) group. I am working on the SLAM project for checking that software satisfies critical properties of the interfaces it uses. SLAM is a part of the SDV tool that is a static analysis tool for Windows drivers, recently released in Vista WDK (Driver Development Kit) as SDV 1.4. I also developed SDV properties for the new model for driver development KMDF, which is also a part of Vista WDK. SDV 1.5, which supports KMDF drivers, will soon be available as a part of Longhorn Server WDK.
I grew up in Russia in the industrial city of Samara, on the banks of the famous Russian river Volga. I attended Department of Computer Science of Lomonosov Moscow State University, where I got my Masters and Ph.D in the area of formal specification of compilers. I worked at the Russian Academy of Sciences at the Keldysh Institute for Applied Mathematics for the Russian Aerospace Space Shuttle BURAN project for more than 10 years, and left Russia after the project was abandoned during perestroika. I spent 1994-1996 at the Middle East Technical University in Ankara, Turkey, working as a researcher in the COST 247 EU project "Verification and Validation Methods for Formal Descriptions". I developed, simulated and verified a formal model of a telephone switch in ITU-T Standard Specification and Description Language (SDL), under a contract with ALCATEL. In 1996, I moved to New Jersey to work on the FormalCheck project at Bell Laboratories. FormalCheck was one of the first commercially available HW verification tools. In 1998, FormalCheck won the Innovation of the Year Award from the EDN magazine. Currently, the tool is marketed by Cadence Design Systems, Inc. for commercial hardware verification, under the trademarks FormalCheck and Incisive Static Verifier (ISV). At Bell Labs, I also developed SDL specification of H.248 MEGACO Voice over IP ITU-T standard protocol. The specification was used for generation of conformance tests for Lucent products. In 2001-2003, I worked with the Wireless Networks Group of Lucent Technologies as a lead of the team engaged into unit, subsystem and feature integration testing of 3G UMTS wireless infrastructure products.