  We propose TOPL automata as a new method for runtime verification of systems
with unbounded resource generation. Paradigmatic such systems are
object-oriented programs which can dynamically generate an unbounded number of
fresh object identities during their execution. Our formalism is based on
register automata, a particularly successful approach in automata over infinite
alphabets which administers a finite-state machine with boundedly many
input-storing registers. We show that TOPL automata are equally expressive to
register automata and yet suitable to express properties of programs. Compared
to other runtime verification methods, our technique can handle a class of
properties beyond the reach of current tools. We show in particular that
properties which require value updates are not expressible with current
techniques yet are naturally captured by TOPL machines. On the practical side,
we present a tool for runtime verification of Java programs via TOPL
properties, where the trade-off between the coverage and the overhead of the
monitoring system is tunable by means of a number of parameters. We validate
our technique by checking properties involving multiple objects and chaining of
values on large open source projects.

Formal Languages and Automata Theory;Software Engineering