2012 | OriginalPaper | Chapter
Thirteen Years of Automated Code Analysis at Microsoft
Author : Wolfram Schulte
Published in: Formal Methods: Foundations and Applications
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Modern program analysis and model-based tools are increasingly complex and multi-faceted software systems. They analyze models and programs using advanced type systems, model checking or model finding, abstract interpretation, symbolic verification or a combination thereof. In this talk I will discuss and compare 10 program analysis tools, which MSR build during the last 10 years. They include theorem provers, program verifiers, bug finders, malware scanners, and test case generators. I will describe the need for their development, their innovation, and application. These tools had both had considerable impact on the research community, as well as being shipped in Microsoft products such as the Static Driver Verifier or as part of Visual Studio and other, widely-used internal software development tools. I highlight that many of these analyzers build on generic infrastructure, most of which is available outside of Microsoft as well. With every analyzer build there is a new opportunity, and with every solution there is a new challenge problem. Thus, I will conclude with 10 challenges in program analysis which hopefully triggers new aspiring directions in our joint quest of delivering predictable software that is free from defect and vulnerabilities.