View: session overviewtalk overview
09:00 | Learning Input Languages for Runtime Verification SPEAKER: Andreas Zeller ABSTRACT. Let us use dynamic tainting to follow the paths of input characters through a program. We will then see that some input fragments end in some variables, and others in others. This allows us to decompose the input into individual parts, one per variable, and consequently, to infer the entire structure of the input as a context-free grammar. In the context of runtime verification, such inferred input grammars have a number of uses. First, they can be used as test drivers, allowing to cover millions of executions in minutes. Second, they can serve to derive dynamic invariants, such as pre- or postconditions. Third, grammars, as well as invariants, can be easily verified dynamically, checking whether inputs and invariants conform to the learned languages. The AUTOGRAM approach will be demonstrated using examples of real programs and (if time permits) even live coding on stage. |
13:30 | Monitoring Hyperproperties SPEAKER: unknown ABSTRACT. We investigate the runtime verification problem of hyperproperties, such as non-interference and observational determinism, given as formulas of the temporal logic HyperLTL. HyperLTL extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. We show that deciding whether a HyperLTL formula is monitorable is PSPACE-complete. For monitorable specifications, we present an efficient monitoring approach. As hyperproperties relate multiple computation traces with each other, it is necessary to store previously seen traces, and to relate new traces to the traces seen so far. If done naively, this causes the monitor to become slower and slower, before it inevitably runs out of memory. In this paper, we present techniques that reduce the set of traces that new traces must be compared against to a minimal subset. Additionally, we exploit properties of specifications such as reflexivity, symmetry, and transitivity, to reduce the number of comparisons. We show that this leads to much more scalable monitoring with, in particular, significantly lower memory consumption. |
14:00 | Monitoring Time Intervals SPEAKER: unknown ABSTRACT. Run-time checking of timed properties requires to monitor events occurring within a specified time interval. In a distributed setting, working with intervals is complicated due to uncertainties about network delays and clock synchronization. Determining that an interval can be closed -- i.e., that all events occurring within the interval have been observed -- cannot be done without a delay. In this paper, we consider how an appropriate delay can be determined based on parameters of a monitoring setup, such as network delay, clock skew and clock rate. We then propose a generic scheme for monitoring time intervals, parameterized by the detection delay, and discuss the use of this monitoring scheme to check different timed specifications, including real-time temporal logics and rate calculations. |
14:30 | Almost Event-Rate Independent Monitoring of Metric Dynamic Logic SPEAKER: Dmitriy Traytel ABSTRACT. Linear temporal logic (LTL) and its quantitative extension metric temporal logic (MTL) are standard languages for specifying system behaviors. Regular expressions are an even more expressive formalism in the non-metric setting and several extensions of LTL, including the recently proposed linear dynamic logic (LDL), offer regular-expression-like constructs. We extend LDL with past operators and quantitative features. The resulting metric dynamic logic (MDL) offers the quantitative temporal conveniences of MTL while increasing its expressiveness. We develop and evaluate an online monitoring algorithm for MDL whose space-consumption is almost event-rate independent---a notion that characterizes monitors that scale to high-velocity event streams. |
Museum of flight
9404 East Marginal Way S.
Seattle, WA 98108
Buses depart in front of Sheraton at 5.30pm.