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.
Since this model incorporates data, the merging process includes a step to ensure that the model remains consistent with the data guards. Each transition in the tree is mapped to its corresponding variable configurations. Pairs of states are only merged if the resulting model completely obeys the data classifiers (guard conditions) that were obtained in the previous step. If the inferred data model predicts that the data value for a given transition is followed by a label @math , any merge involving the target state can only occur if the resulting state machine contains an outgoing transition that is labelled by @math . After each merge, the resulting state machine is further post-processed to ensure that each transition is deterministic @cite_12 .
@cite_12
1549166962
A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.