* SPARKSkein released
@ 2010-08-16 7:37 Rod Chapman
2010-08-16 11:42 ` Peter C. Chapin
2010-08-16 16:18 ` Yannick Duchêne (Hibou57)
0 siblings, 2 replies; 3+ messages in thread
From: Rod Chapman @ 2010-08-16 7:37 UTC (permalink / raw)
Altran Praxis and AdaCore have released SPARKSkein - a new reference
implementation of Skein-512 written and verified using the SPARK
language and toolset. In particular, this release includes a complete
proof of type-safety for the implementation, test cases for structural
coverage, performance, and the reference test vectors from the Skein
specification. Performance is very close to that of the C reference
implementation.
Check it out at www.skein-hash.info
There's also a technical paper describing the implementation and
results, available from
the same place.
- Rod Chapman, SPARK Team, Altran Praxis
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: SPARKSkein released
2010-08-16 7:37 SPARKSkein released Rod Chapman
@ 2010-08-16 11:42 ` Peter C. Chapin
2010-08-16 16:18 ` Yannick Duchêne (Hibou57)
1 sibling, 0 replies; 3+ messages in thread
From: Peter C. Chapin @ 2010-08-16 11:42 UTC (permalink / raw)
On 2010-08-16 03:37, Rod Chapman wrote:
> Altran Praxis and AdaCore have released SPARKSkein - a new reference
> implementation of Skein-512 written and verified using the SPARK
> language and toolset...
This is great! Thanks for pointing it out.
Peter
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: SPARKSkein released
2010-08-16 7:37 SPARKSkein released Rod Chapman
2010-08-16 11:42 ` Peter C. Chapin
@ 2010-08-16 16:18 ` Yannick Duchêne (Hibou57)
1 sibling, 0 replies; 3+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-08-16 16:18 UTC (permalink / raw)
Le Mon, 16 Aug 2010 09:37:59 +0200, Rod Chapman
<roderick.chapman@googlemail.com> a écrit:
> Altran Praxis and AdaCore have released SPARKSkein - a new reference
> implementation of Skein-512 written and verified using the SPARK
> language and toolset. In particular, this release includes a complete
> proof of type-safety for the implementation, test cases for structural
> coverage, performance, and the reference test vectors from the Skein
> specification. Performance is very close to that of the C reference
> implementation.
>
> Check it out at www.skein-hash.info
>
> There's also a technical paper describing the implementation and
> results, available from
> the same place.
>
> - Rod Chapman, SPARK Team, Altran Praxis
Was useful:
http://www.skein-hash.info/sites/default/files/SPARKSkein.pdf
says
> [...]
> 4.1.1 Prover says no…a bug is discovered
> The subprogram Skein_512_Final caused someproblems, and led to the
> discovery of a subtle
> corner-case bug.
> [...]
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2010-08-16 16:18 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-08-16 7:37 SPARKSkein released Rod Chapman
2010-08-16 11:42 ` Peter C. Chapin
2010-08-16 16:18 ` Yannick Duchêne (Hibou57)
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox