Verification of parameterized systems by induction

A parameterized system is an infinite family of finite-state systems. The goal of this project is to extend the finite-state logic programming based model-checker (called XMC) to verify temporal properties of parameterized systems. XMC is a finite-state algorithmic model-checker which is encoded in a deductive setup. It's execution is based on an evaluation strategy which could be roughly seen as memoized resolution. In program transformation terminology, XMC performs model-checking by repeated unfolding steps using the encoding of the structural operational semantics of CCS and modal mu calculus.

We seek to extend the underlying evaluation mechanism of XMC for verification of parameterized concurrent systems. We do so by :

• employing more powerful program transformation rules such as folding or goal replacement. These transformations correspond to deductive steps.
• imparting more control into the unfolding transformation, so as to prevent infinite unfolding.

Related documents :

• Verification of Parameterized Systems using Logic Program Transformations,
  by A. Roychoudhury, K. Narayan Kumar,C.R. Ramakrishnan, I.V. Ramakrishnan and S.A. Smolka,
  Accepted for TACAS 2000.
  
• Proofs by Program Transformations ,
  by A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan
  In Pre-proceedings of Logic-based Program Synthesis and Transformation (LOPSTR) '99.
  
• A parameterized unfold/fold transformation framework for definite logic programs,
  by A. Roychoudhury, K. Narayan Kumar, C.R. Ramakrishnan, I.V. Ramakrishnan
  International Conference on Principles and Practice of Declarative Programming (PPDP) LNCS 1702, pages 396-413, 1999..
  
• Tabulation based Induction Proofs with Applications to Automated Verification ,
  by A. Roychoudhury, C.R. Ramakrishnan, I.V. Ramakrishnan and S.A. Smolka,
  International Workshop on Tabulation in Parsing and Deduction, 1998.