Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
d5e242e3
Commit
d5e242e3
authored
Feb 15, 2020
by
Benoit Viguier
Browse files
commented-added: verification person-month
parent
bb892287
Changes
1
Hide whitespace changes
Inline
Side-by-side
paper/6-conclusion.tex
View file @
d5e242e3
...
...
@@ -77,6 +77,20 @@ adjustments do not impact the trust of our proof.
We contacted the authors of TweetNaCl and expect that the changes described
above will soon be integrated in a new version of the library.
% Do we want to say that ?
% \subheading{Verification Effort.}
% In addition to the time required to get familiar with
% research software, we faced a few bugs which we reported
% to the developers of the VST to get them fixed.
% It is very hard to work with a tool without being involved
% in the development loop. Additionally newer versions often
% broke some of our proofs and it was often needed to adapt
% to the changes.
% As a result we do not believe the metric person-month to be
% a good representation of the verification effort.
\subheading
{
Extending our work.
}
The high-level definition (
\sref
{
sec:maths
}
) can easily be ported to any
other Montgomery curves and with it the proof of the ladder's correctness
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment