Mining finite-state automata with annotations

Many software design and verification techniques assume the availability of some kind of behavioral models of the systems under analysis [2,4,10,11,28]. Unfortunately, manually specifying and maintaining behavioral models is expensive and error prone, and requires specific skills that are not always available in development teams. This reduces the applicability of model-based approaches in industrial projects. The problem of generating behavioral models can be solved with techniques that automatically generate behavioral models by mining program executions and thus reducing the effort required to generate models [3, 5, 18,20,24]