@techreport{atr42,
author = {Klaus Dr{\"a}ger and Bernd Finkbeiner},
title = {Subsequence Invariants},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {S1},
year = {2008},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 42,
note = {ISSN: 1860-9821, http://www.avacs.org.},
access = {open},
abstract = {We introduce subsequence invariants, which characterize
the behavior of a concurrent system in terms of the
occurrences of synchronization events. Unlike state
invariants, which refer to the state variables of the
system, subsequence invariants are defined over auxiliary
counter variables that reflect how often the event
sequences from a given set have occurred so far. A
subsequence invariant is a linear constraint over the
possible counter values. We allow every occurrence of a
subsequence to be interleaved arbitrarily with other
events. As a result, subsequence invariants are preserved
when a given process is composed with additional processes.
Subsequence invariants can therefore be computed
individually for each process and then be used to reason
about the full system. We present an efficient algorithm
for the synthesis of subsequence invariants. Our
construction can be applied incrementally to obtain a
growing set of invariants given a growing set of event
sequences.},
bibtex = {atr042.bib},
pdf = {avacs_technical_report_042.pdf}
}