A synchronous observer is an adjunct to a system model that monitors its state variables and raises a signal when some condition is satisfied. Synchronous observers provide an alternative to temporal logic as a means to specify safety properties but have the benefit that they are expressed in the same notation as the system model. Model checkers that do use temporal logic can nonetheless employ synchronous observers by checking for properties such as "never(signal raised)." The use of synchronous observers to specify properties is well-known; rather less well-known is that they can be used to specify assumptions and axioms, to constrain models, and to specify test cases. The idea underlying all these applications is that the basic model generates more behaviors than are desired, the synchronous observer recognizes those that are interesting, and the model checker is constrained to just the interesting cases. The value in this approach is that it is usually much easier to write recognizers than generators. The approach is best exploited in languages such as SAL that provide explicit first class operators for synchronous and asynchronous composition. The paper describes and illustrates these applications of synchronous observers.

Automated code analysis is technology aimed at locating, describing and repairing areas of weakness in code. Code weaknesses range from security vulnerabilities, logic errors, concurrency violations, to improper resource usage, violations of architectures or coding guidelines. Common to all code analysis techniques is that they build abstractions of code and then check those abstractions for properties of interest. For instance a type checker computes how types are used, abstract interpreters and symbolic evaluators check how values flow, model checkers analyze how state evolves. Building modern program analysis tools thus requires a multi-pronged approach to find a variety of weaknesses.
In this talk I will discuss and compare several program analysis tools, which MSR build during the last ten 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. Many of these tools had considerable impact on Microsoft's development practices, as well as on the research community. Some of them are being shipped in products such as the Static Driver Verifier or as part of Visual Studio.
Performing program analysis as part of quality assurance is meanwhile standard practice in many software development companies. However several challenges have not yet been resolved. Thus, I will conclude with a set of open 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.