kth-tcs/trustfull-demonstrator

document the verification of the vote collection server

Opened this issue · 0 comments

we design a minimal functionality version of the vote collection server in cakeml and we synthesize the code from it (ongoing project)

possibly, we would call this synthesized component from within Java (i.e. we would replace the Java submodule by the synthesizer)

(i.e. we do not verify the current Java implementation of the vote collection)

cc/ @palmskog