IPSG: Invariant Proof Score Generator
Duong Dinh Tran, Kazuhiro Ogata · 2022 IEEE 46th Annual Computers, Software, and Applications Conference (COMPSAC) · 2022
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.