Invited Speakers

Trishul M. Chilimbi

Runtime Analysis and Design Research
Microsoft Research

Asymptotic Runtime Verification through Lightweight Continuous Program Analysis

Abstract
We describe a runtime program analysis infrastructure that is able to capture and analyze fine-grain program behavior including rare events while incurring very low runtime overhead. The lightweight nature of the runtime analysis framework makes it a viable candidate for inclusion in production software and permits continuous program analysis. This enables the analysis to explore a growing number of feasible program paths and increase coverage of the space of input data values. Given a sufficiently large software user base and a long enough time period, asymptotic verification of analyzed program properties may be achieved. To support our claims, we present experimental data for a leak detection tool--SWAT--that has been implemented using this infrastructure and used internally at Microsoft by several product groups over a period of two years.



Klaus Havelund

Kestrel Technology

Runtime Verification Languages

Abstract
Runtime verification is currently trying to establish itself as a field of its own. The objective of this field is to study and develop languages, algorithms and environments for monitoring the execution of computer programs, or more generally: evolving systems. One specific branch of this field is specification-based runtime verification where a program run, generating a trace, is monitored against a specification that denotes the set of correct traces. This specification can potentially just be another program that evaluates the events generated by the observed program. Alternatively, it can be a term in some simple and clean temporal logic. The former solution is flexible and expressive but may result in too low-level specifications. The latter solution often results in very succinct specifications, but it may in many cases also result in unreadable specifications due to the limited set of constructs available. Furthermore, it may not be expressive enough for practical purposes. We present some thoughts on the middle ground between these two extremes. That is, between the "general purpose program" solution and the "simple logic" solution. As an illustration, the Eagle specification language will be presented as a logic-based version of the more general "program" solution, trying to achieve the benefits of both worlds: expressiveness, specification succinctness, and simplicity of the notation.