Distinguishing Formulas for Free

T. Margaria, B. Steffen

	   A system for the efficient verification of the input/output
	   correctness of Finite State Machines with data path and
	   control unit is presented. This system, which is based on
	   First-Order Logic theorem proving, is unique in automatically
	   providing distinguishing formulas expressing all test
	   patterns that witness a behavioural difference between two
	   descriptions. Experimental results illustrate the test pattern
	   generation feature for stuck-at faults, functional faults,
	   and initialization faults, and the efficiency which results
	   from the compositionality of the verification.