Proof System Violet Based on Tecton
Jie Zhai · Huadong Li-Gong Daxue xuebao · 2005
On the basis of Tecton specifications of component concepts, we build verification system Violet to prove properties of components automatically. Violet is a tool based on rewriting techniques. Its main goal is to help the user find proofs and understand proofs and build libraries of verified software or hardware components. We describe the novel features of Violet in the aspects of proof visualization and proof automation. At last we present the Tecton specification and Violet verification of the alternating bit protocol.