@inproceedings{havelund-rosu-2002-tacas,
author = {Klaus Havelund and Grigore Rosu},
title = {Synthesizing Monitors for Safety Properties},
abstract = {
The problem of testing a linear temporal logic (LTL) formula on a
finite execution trace of events, generated by an executing program,
occurs naturally in runtime analysis of software. An
algorithm which takes a past time LTL formula and generates an
efficient dynamic programming algorithm is presented. The
generated algorithm tests whether the formula is satisfied by a
finite trace of events
given as input and runs in linear time, its
constant depending on the size of the LTL formula. The memory needed
is constant, also depending on the size of the formula.
Further optimizations of the algorithm are suggested.
Past time operators suitable for writing succinct
specifications are introduced and shown definitionally equivalent to
the standard operators. This work is part of the PathExplorer
project, the objective of which it is to construct a flexible
framework for monitoring and analyzing program executions.
},
booktitle = {Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02)},
pages = {342-356},
month = {April},
year = {2002},
series = {LNCS},
volume = {2280},
publisher = {Springer},
author_id = {Klaus Havelund and Grigore Rosu},
category = {javamop,runtime_verification},
project_url = {https://github.com/runtimeverification},
project_name = {MOP},
booktitle_acronym = {TACAS'02},
booktitle_url = {http://www.etaps.org/2002/Tacas/tacas.html},
doi = {http://dx.doi.org/10.1007/3-540-46002-0_24},
presentation = {2002-04-TACAS},
}