Charla: “Clara: Partially evaluating runtime monitors at compile time”



Charlista: Eric Bodden, Technical University of Darmstadt, Germany


Organiza PLEIAD


Día: miércoles 10 de noviembre
Hora: 12.00 hrs. 
Lugar: Auditorio DCC, tercer piso.




Finite-state runtime monitors allow programmers to conveniently describe, find and prevent execution sequences that would violate safety or security properties. However, pure runtime monitoring suffers from the fact that it can (1) introduce a large runtime overhead, and (2) requires good test coverage to uncover possible software errors with confidence. In general, runtime monitoring can, as testing in general, only prove the presence of errors, not their absence.


We therefore present Clara, a novel static-analysis framework for partially evaluating runtime monitors at compile time. Clara uses a sequence of increasingly precise static analyses to automatically convert a runtime monitor into a residual runtime monitor. The residual monitor only watches events triggered by program locations that the analyses failed to prove safe at compile time. In two-thirds of the cases in our large-scale experiments, the static analysis succeeds on all locations, proving that the program fulfills the stated properties, and completely obviating the need for runtime monitoring. In the remaining cases, the residual runtime monitor is usually much more efficient than a full monitor, yet still captures all property violations at runtime.


We implemented Clara as an open framework to combine research from the runtime-verification and static-analysis communities. As Clara can operate on all runtime monitors that have the form of AspectJ aspects, it integrates with most current runtime-verification tools. Further, researchers can easily enhance Clara with new static analyses that can then automatically optimize monitors generated by any of these tools.




Eric Bodden received his Diplom from RWTH Aachen University, Germany, in 2005. Having completed his doctoral dissertation at the Sable Research Group at McGill University, Montreal, Canada, Eric now continues his research as a Postdoctoral Fellow at the Technical University Darmstadt, Germany. Eric's research interests include static and dynamic analyses that allow programmers to reason about large-scale object-oriented programs. For his dissertation, Eric developed Clara, a framework for evaluating finite-state runtime monitors at compile time. Eric seeks applied solutions, combining compilation and sound static program analysis techniques with unsound and incomplete techniques from Software Engineering. Early on, Eric recognized the potential of aspect-oriented programming as a convenient abstraction for program analysis and verification.


Comunicaciones DCC