Oleg Sokolsky
Computer Science Department
University of Pennsylvania
"Runtime Verification "
Abstract
Run-time verification is a dynamic analysis technique that has emerged in recent years. Run-time verification targets system models that are too complex to be exhaustively analyzed by model checking, or system implementations that do not have models suitable for verification. Instead of exploring the whole state space of the system, run-time verification techniques check system executions with respect to a set of formally specified requirements. Run-time verification resorts to instrumentation or other kinds of execution monitoring to extract a trace of observations and then applies formal verification to this trace. Execution of recovery code upon discovering a violation makes it possible to provide feedback to the running system.
Tuesday, November 18, 2008
3:00 - 4:15
Wu & Chen
101 Levine Hall