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] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)