Verification of parameterized programs
Zohar Manna, Amir Pnueli · 1995
Introduction In this chapter we present an approach to the verification of parameterized reactive programs, using temporal logic 1 . A parameterized program consists of several similar processes whose number is determined by an input parameter. A challenging problem is to provide methods for the uniform verification of such programs, i.e., proving correctness of the program for any number of processes. The ability to conduct a uniform verification of a parameterized program is one of the striking advantages of the deductive method for temporal verification over model-checking techniques such as [2] and [1]. Let M denote the input parameter which determines the number of processes in the considered system. We can use model-checking to verify the desired properties of the system for specific values of M , such as M = 3; 4; 5. Usually, the model checke