e Abstractions for Parameterized Systems JOXAN JAFFAR and ANDREW E. SANTOSA Department of Computer Science, National University of Singapore Singapore 117590 {joxan,andrews}comp.nus.edu.sg We consider a language of recursively defined formulas about arrays of variables, suitable for specifying safety properties of parameterized systems. We then present an abstract interpretation framework which translates a paramerized system as a symbolic transition system which propagates such formulas actions of underlying concrete states. The main contribution is a proof method for implications between the formulas, which then provides for an implen of this abstract interpreter.
Joxan Jaffar, Andrew E. Santosa