@techreport{rosu-havelund-2001-tr,
author = {Grigore Rosu and Klaus Havelund},
title = {Synthesizing Dynamic Programming Algorithms from Linear Temporal Logic Formulae},
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. We present an
algorithm which takes an LTL formula and generates an efficient
dynamic programming algorithm. The generated algorithm tests whether
the LTL formula is satisfied by a finite trace of events given as
input. The generated algorithm 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.
},
institution = {Research Institute for Advanced Computer Science},
month = jan,
year = {2001},
number = {https://ti.arc.nasa.gov/m/pub-archive/archive/0220.pdf},
author_id = {Grigore Rosu and Klaus Havelund},
category = {logics,programming_languages,runtime_verification,javamop},
hidden = {false},
}