Verification as a parameterized testing (experiments with the SCP4 supercompiler)
Alexei Lisitsa, Andrei P. Nemytykh · Programming and Computer Software · 2007
Let a program-predicate t testing another program p with respect to a given postcondition be given. Concrete tests d (data of the program p ) are input data for t . Let us consider the program t when values of its argument d are unknown. Then a proof of the fact that the prediate t is true for all input data of the program p is verification of p with respect to the given postcondition. In this paper, we describe experiments on automatic verification of a number of cache coherence protocols with the SCP4 supercompiler (an optimizer of programs written in the REFAL-5 functional language).