Verification of Parameterized Systems Using Logic Program Transformations

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


Abstract:

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:

@inproceedings{RKRRS:TACAS00,
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
(cram@cs.sunysb.edu)