|Advanced Techniques for Software Reliability|
These non-interference properties will be examined in the context of type systems because they often provide the best balance between ease-of-use, scalability, and expressiveness. Specific topics include the theoretical foundations and implementation issues surrounding these systems, as well as type inference algorithms for them. We will also discuss our experiences with prototype checkers and alternative approaches based model-checking, dynamic analysis, and theorem proving.
However, if the property does not hold of the abstraction along some trace T (a counterexample), it may or may not hold of the original program on trace T. If it can be proved that the property does not hold in the original program on trace T then it makes sense to refine the abstraction to eliminate the "spurious counterexample" T (rather than a report a known false negative to the user).
The SLAM project at Microsoft Research pioneered the automated abstraction-refinement process for software and applied it to the domain of device drivers. In this series of lectures, I reformulate the process for a tiny while language using the concepts of weakest preconditions, bounded model checking and Craig interpolants. This representation of SLAM distills the concepts of counterexample-driven refinement in a simple form.
We then extend the method to multithreaded systems, where concurrency errors are hard to detect and reproduce. To do so, we use LA to automatically infer a succinct model of how each thread affects other threads, and then automatically verify the full system by composing the models . The technique was applied to analyze device drivers and Networked Embedded Systems code for data races.
Finally we describe how LA can be used to facilitate modular program analysis, by automatically synthesizing from a library, a stateful interface (i.e. a typestate system), which can then be used (instead of the library) to check if a given client uses the library correctly.
Although proper blame assignment has been a key aspect of contract checking since its beginnings, getting blame right has proven to be difficult. In the early days of first-order functional programming, blame assignment was a simple matter. As programming languages have become more sophisticated, however, proper blame assignment has not kept pace. Indeed, the most widely used and imitated contract checker, Eiffel, incorrectly assigns blame. Worse, until recently, there was no way to properly assign blame for contract checkers in languages with structural subtyping or higher-order functions.
We will explain contract checking, demonstrating how a focus on proper blame assignment leads to well-designed, useful contract checkers .
|This page is the property of the University of Oregon|