Interactive theorem provers have been used extensively to reason about various software hardware systems and mathematical theorems. The key challenge when using an interactive prover is finding a suitable sequence of proof steps that will lead to a successful proof requires a significant amount of human intervention. This paper presents an automated technique that takes as input examples of successful proofs and infers an Extended Finite State Machine as output. This can in turn be used to generate proofs of new conjectures. Our preliminary experiments show that the inferred models are generally accurate (contain few false-positive sequences) and that representing existing proofs in such a way can be very useful when guiding new ones.
EFSMInfer has several optional parameters. The most important parameter is the choice of data classifier algorithm, which is used to infer the guards on the transitions. For this, EFSMInfer incorporates several standard algorithms that were implemented as part of the Weka @cite_11 toolset. In our experiments, we will adopt the default parameters in EFSMInfer.
@cite_11
2125364373
Markov chains with Labelled Transitions can be used to generate test cases in a model-based approach. These test cases are generated by random walks on the model according to probabilities associated with transitions. When these probabilities correspond to a usage profile, reliability may be estimated. However, in early stages of development, such probabilities are not easy to determine, thus default profiles must be considered. In such a case it may be interesting to target some coverage criteria rather to use classical uniform probability generation approach. In this paper we enrich an existing industrial tool based on usage profile with 3 possibilities to create default profiles that improve transition coverage. We report experiments that compare the improvement of the coverage rates by our approaches with respect to uniform probabilities on transitions from a given state, which is the current default profile.