Verification of Parameterized Systems Using Logic Program Transformations

Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, Scott A. Smolka


We show how the problem of verifying parameterized systems can be reduced to the problem of determining the equivalence of goals in a logic program. We further show how goal equivalences can be established using induction-based proofs. Such proofs rely on a powerful new theory of logic-program transformations (encompassing unfold, fold and goal replacement over multiple recursive clauses), can be highly automated, and are applicable to a variety of network topologies, including uni- and bi-directional chains, rings, and trees of processes. Unfold transformations in our system correspond to algorithmic model-checking steps, fold and goal replacement correspond to program deductions, and all three types of transformations can be arbitrarily interleaved within a proof. Our framework thus provides a seamless integration of algorithmic and deductive verification at fine levels of granularity.

Bibtex Entry:

author = {Abhik Roychoudhury and  K. Narayan Kumar and  C. R. Ramakrishnan and  I. V. Ramakrishnan and  Scott A. Smolka},
title = {Verification of Parameterized Systems Using Logic Program Transformations},
booktitle = {Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems ({TACAS})},
address = {Berlin, Germany},
month = {March},
series = {Lecture Notes in Computer Science},
volume = {1785},
publisher = {Springer},
pages = {172--187},
year = {2000}

Full Paper: [pdf]

Home | Papers

C. R. Ramakrishnan