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

Hantao Zhang