Re: Sponsor this

[Sven LUTHER <luther@dpt-info.u-strasbg.fr>]

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