VOTE Group Editors Analyzing Tool

AbstractWe present an initial version of a tool VOTE1 for detecting copies inconsistency in group editors. As input, our tool takes an algorithmic-description which consists of the group editor behaviour and the transformation algorithm. VOTE translates this description into rewrite rules. As a verification back-end we use SPIKE, an automated induction-based theorem prover, which is suitable for reasoning about conditional theories. The effectiveness of our tool is illustrated on several case studies. 1VOTE can be found at http://www-sop.inria.fr/coprin/urso/logiciels/