The contest will be held offline before the workshop and due to the intrinsic complexity of any standard of comparison there will be no official winner. Each team will be expected to fill in a questionaire explaining their results, e.g the rate of success, the rate of interactions, the time spent for each example, the behaviour on non-provable examples etc. Each team will be expected to run its system during the workshop. A sample of examples will be arranged from the testbed and will be given to the systems online during the workshop verifying the proposed results. Formal program development is becoming a mature and established discipline with a dynamic and increasing market share.
Induction is one of the key techniques when dealing with abstract datatypes.
The aim of this session is to bring together the merits of inductive theorem proving techniques and the needs of formal methods in an industrial application scenario. The aim of this session is to address the adequacy of current automated techniques for inductive proof within the context of higher-order logics. Here we are also interested in problems which demonstrate the unique merits of inductive theorem proving techniques. Submitted challenge problems will be displayed on the Web prior to the workshop. Researchers will then be invited to submit solutions or counter challenges.