"The SPARK Way to Correctness is via Abstraction" John Barnes, Presented at Sig-Ada 2000.
(2000)
Languages mentioned
SPARK95
{1999} Provable Ada95