Write a Blog >>
Tue 20 Jun 2017 16:55 - 17:30 at Vertex WS217 - D Chair(s): Radu Grigore

Parametric trace expressions are a formalism expressly de- signed for parametric runtime verification (RV) which has been introduced and successfully employed in the context of runtime monitoring of multiagent systems.

Trace expressions are built on the general notion of event type, which allows them to be adopted in different contexts. In this paper we show how trace expressions can be used for conveniently specifying the expected behavior of a Java-like program to be monitored at runtime.

Furthermore, we investigate the basic properties of the primitive operators on which trace expressions are coinduc- tively defined in terms of a labeled transition system; this provides a basis for formal reasoning on equivalence of trace expressions and adopting useful optimization techniques to speed up runtime verification.

Tue 20 Jun
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00: DFTfJP at Vertex WS217
Chair(s): Radu GrigoreUniversity of Kent
16:00 - 16:20
Consistency Types for Safe and Efficient Distributed Programming
Alessandro MargaraPolitecnico di Milano, Guido SalvaneschiTU Darmstadt
16:20 - 16:55
Correctness of Partial Escape Analysis for Multithreading Optimization
Dustin Rhodes, Cormac FlanaganUniversity of California, Santa Cruz, Stephen N. FreundWilliams College
16:55 - 17:30
Parametric trace expressions for runtime verification of Java-like programs
Davide AnconaUniversity of Genova, Angelo Ferrando, Luca FranceschiniDIBRIS, University of Genova, Italy, Viviana MascardiDIBRIS, University of Genova, Italy