IPSG: Invariant Proof Score Generator

Many previous case studies on formal verification of invariant properties by writing proof scores have demonstrated that the approach is powerful and flexible. Writing proof scores by hand, however, is prone to human errors and time-consuming, especially with complicated systems or specifications. Therefore, we propose an approach and implement a tool (called Invariant Proof Sore Generator or IPSG) that can automatically generate proof scores for formal invariant property verification. We demonstrate the practicability of the tool with three mutual exclusion protocols and one authentication protocol. The experiments show that IPSG can completely generate proof scores to prove that those protocols enjoy some desired properties.