Investigating Program Behavior Using the Texada LTL Specifications Miner

Temporal specifications, relating program events through time, are useful for tasks ranging from bug detection to program comprehension. Unfortunately, such specifications are often lacking from system descriptions, leading researchers to investigate methods for inferring these specifications from code, execution traces, code comments, and other artifacts. This paper describes Texada, a tool to dynamically mine temporal specifications in LTL from traces of program activity. We review Texada´s key features and demonstrate how it can be used to investigate program behavior through two scenarios: validating an implementation that solves the dining philosophers problem and supporting comprehension of a stack implementation. We also detail Texada´s other, more advanced, usage options. Texada is an open source tool: https://bitbucket.org/bestchai/texada.