Tags:Invariant checking, Invariant generation, Local theory extensions, SMT and Symbol elimination
Abstract:
In this paper we study possibilities for automated invariant generation in parametric systems. For this, we refine results on symbol elimination we previously established in order to make them more efficient. We use these results for devising 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 method on several examples.