# On Invariant Synthesis for Parametric Systems

## TL;DR

This paper presents a method for automated invariant synthesis in parametric systems using a refined symbol elimination algorithm, with conditions for correctness, completeness, and termination, demonstrated through examples.

## Contribution

It introduces a novel approach combining symbol elimination with invariant strengthening for parametric systems, including correctness and termination guarantees.

## Key findings

- Method successfully synthesizes invariants in various examples.
- Conditions for correctness and termination are established.
- Approach enhances automation in safety property verification.

## Abstract

We study possibilities for automated invariant generation in parametric systems. We use (a refinement of) an algorithm for symbol elimination in theory extensions to devise a method for iteratively strengthening certain classes of safety properties to obtain invariants of the system. We identify conditions under which the method is correct and complete, and situations in which the method is guaranteed to terminate. We illustrate the ideas on various examples.