On Tue, Dec 19, 2000 at 07:23:35PM +1000, Anthony Towns wrote: > On Tue, Dec 19, 2000 at 09:43:27AM +0100, Sven LUTHER wrote: > > What about writing some kind of code that resolve the vote in some kind of > > easy to prove language, and then do some program property proofs on it ? > > I'm not sure why this helped (because I didn't do it), but it did.
Actually i was speaking of algorythm proofing using some kind of program prover. I am not an expert in the domain, but i know it has been used succesfully for various kind of stuff (like proving chip architecture, or automated train systems) . Compared to that, the resolution of a voting procedure is a somewhat simple algorythm, i think, so it could be studied and properties prooved on it quite easily, i guess. Friendly, Sven Luther
