Foundations of Software Engineering - Home
The goal of the Foundations of Software Engineering (FSE) group at Microsoft Research in Redmond, Wash., is to improve software development productivity by using automated software verification.
The term automated software verification refers to machine-assisted techniques that compare the actual behavior of a software component with its predicted behavior. Verification can occur at design time or during the program’s execution. Whether static or dynamic, automated verification always operates with respect to a notion of predicted system behavior, which is typically expressed in the form of a specification. Specifications may be generic, for instance the code should not crash, or can be specific to the system.
Specification-based software verification can occur at three levels of detail: the system or architecture level, the unit or class level and the source code level. Benefits of introducing specifications are numerous: they document design decisions, they enable early automatic analysis of designs, they enable test to start much earlier, and they allow automatic test case generation and execution.