Finite Model Generation

Mathematical induction is required for reasoning about objects or events containing repetition, e.g. computer programs with recursion or iteration, electronic circuits with feedback loops or parameterized components. Thus automating mathematical induction is a key enabling technology for the use of formal methods in information technology. Failure to automate inductive reasoning is one of the major obstacles to the widespread use of formal methods in industrial hardware and software development. In the last ten years, we implemented two methods based on the approach of proof by consistency in the prover RRL. We also developed a method based on the concept of cover set for mechanizing proofs by explicit induction for equational specifications. We have used the cover-set method for software verification and hardware verification.

The code of RRL

Papers on Automated Induction

System Development

• Kapur, D., Zhang, H.: (1995) An overview of Rewrite Rule Laboratory . Journal of Mathematics of Computation.
• Kapur, D., Zhang, H.: (1994) Automated induction: explicit vs. implicit (abstract) In Proc. of Third International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida. The full paper is available upon request.
• Zhang, H., Hua, G.X.: (1993) Proving Ramsey theorem by the cover set induction: a case and comparison study . The Annals of Mathematics and Artificial Intelligence, Volume 8, (1993) 383-405.
• Hua, G.X., Zhang, H.: (1992) FRI: Failure Resistant Induction in RRL . In Kapur, D.: (ed.): Proc. of 1992 International Conference of Automated Deduction. Saratoga, NY. Lecture Notes in Artificial Intelligence, 607, Springer-Verlag. pp. 691--695.
• Kapur, D., Narendran, P., Zhang, H.: (1991) Automating inductionless induction by test sets . J. of Symbolic Computation}, 11, 83-111.
• Zhang, H. (ed.): Automated Mathematical Induction, April 1996, 224 pp. Kluwer Academic Publishers.

  Software Design Verification

• Lee, K., Zhang, H.: (1995) Formal development of a register allocation algorithm . Technical Report, Dept. of Computer Science, UI.
• Zhang, H., Hua, G.X.: (1992) Proving the Chinese remainder theorem by the cover ste induction . In Kapur, D.: (ed.): Proc. of 1992 International Conference of Automated Deduction. Saratoga, NY. Lecture Notes in Artificial Intelligence, 607, Springer-Verlag. pp. 431--445.

  Hardware Design Verification

• Hua, G.X., Zhang, H.: (1993) Formal verification of circuit designs in VHDL . In Proc. of 9th International Conference on Advanced Science and Technology, Motorola, Inc., Schaumburg, Illinois.
• Hua, G.X., Zhang, H.: (1992) Axiomatic semantics of a hardware specification language . In Proc. of the Second IEEE Great Lakes Symposium on VLSI Design. Kalamazoo, MI. pp. 183-190.