Personal tools
You are here: Home Events ICSA COLLOQUIUM TALK


— filed under:

Presentation and talk by Prof Patrick Lam, University of Waterloo, Canada. Title: Static and Dynamic Verification of Finite-State Properties.

  • Colloquium Series
When Jan 18, 2012
from 04:00 PM to 05:00 PM
Where Informatic Forum 4.31/4.33
Add event to calendar vCal


 Finite-state properties account for an important class of program  properties, typically related to the order of operations invoked on  objects. Many library implementations therefore include manually-written finite-state monitors to detect violations of finite-state properties at runtime. Researchers have recently proposed the explicit specification of finite-state properties and automatic generation of monitors from the specification.

Runtime monitoring shows the presence of violations, given appropriate test cases; however, it typically cannot prove their absence. Moreover, inserting a runtime monitor into a program under test can slow down the program by several orders of magnitude. We present an application of dynamic binary instrumentation (using the Pin framework) to runtime monitoring of finite-state properties on x86 binaries.

We also present a set of four static whole-program analyses that partially evaluate runtime monitors at compile time, with increasing cost and precision. As we show, ahead-of-time evaluation can often evaluate the monitor completely statically. This may prove that the program cannot violate the property on any execution or may prove that violations do exist. In the remaining cases, the partial evaluation converts the runtime monitor into a residual monitor. This monitor only receives events from program locations that the analyses failed to prove irrelevant. This makes the residual monitor much more efficient than a full monitor, while still capturing all property violations at runtime.

We implemented the static analyses in Clara, a novel framework for the partial evaluation of AspectJ-based runtime monitors, and validated  our approach by applying Clara to finite-state properties over several large-scale Java programs. Clara proved that most of the programs  never violate our example properties. Some programs required monitoring, but in those cases Clara could often reduce the monitoring overhead to below 10%. We observed that several programs did violate the stated properties.

This is joint work with Jon Eyolfson, Eric Bodden, and Laurie Hendren.



Patrick Lam is an Assistant Professor at the University of Waterloo, and a Visiting Scholar at the University of California, Berkeley. His research interests include program analysis and the design and verification of lightweight specification languages. His non-research interests include activities with elevation gain/loss and technical gear.

Document Actions