We investigate the problem of safety verification of infinite-state parameterized programs that are formed based on a rich class of topologies. We introduce a new proof system, called parametric proof spaces, which exploits the underlying symmetry in such programs. This is a local notion of symmetry which enables the proof system to reuse proof arguments for isomorphic neighbourhoods in program topologies. We prove a sophisticated relative completeness result for the proof system with respect to a class of universally quantified invariants. We also investigate the problem of algorithmic construction of these proofs. We present a construction, inspired by classic results in model theory, where an infinitary limit program can be soundly and completely verified in place of the parameterized family, under some conditions. Furthermore, we demonstrate how these proofs can be constructed and checked against these programs without the need for axiomatization of the underlying topology for proofs or the programs. Finally, we present conditions under which our algorithm becomes a decision procedure.

翻译：我们研究了基于丰富拓扑结构构建的无限状态参数化程序的安全性验证问题。我们提出了一种称为参数化证明空间的新型证明系统，该系统利用了此类程序中固有的对称性。这是一种局部对称性概念，使得证明系统能够在程序拓扑结构中为同构邻域复用证明论证。我们针对一类全称量化不变式，为该证明系统证明了一个精密的相对完备性结果。同时，我们研究了这些证明的算法构造问题。受模型论经典成果启发，我们提出了一种构造方法：在某些条件下，可以通过对无穷极限程序进行完备且可靠验证来替代对整个参数化程序族的验证。此外，我们展示了如何无需对底层拓扑结构进行公理化处理，即可针对这些程序构造并验证此类证明。最后，我们提出了使算法成为判定程序所需满足的条件。