Checking LTL[F, G, X] on compressed traces in polynomial time

Minjian Zhang, Umang Mathur, Mahesh Viswanathan

Abstract

The problem of checking if a program execution meets a formal specification arises in many software engineering tasks including runtime verification and designing test oracles. When online analysis is not possible, execution trace logs are stored for offline postmortem analysis, often in a compressed format to reduce disk space and warehousing requirements. A straightforward method for checking if a compressed execution satisfies a property is to first decompress it and then analyze the resulting uncompressed execution.

BibTeX

@inproceedings{Zhang-al:FSE21,
  author    = {Minjian Zhang and
               Umang Mathur and
               Mahesh Viswanathan},
  title     = {Checking {LTL[F,} G, X] on compressed traces in polynomial time},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {131--143},
  publisher = {{ACM}},
  year      = {2021},
}

Checking LTL[F, G, X] on compressed traces in polynomial time

Abstract

Related papers