Using the SPARK Toolset for Showing the Absence of Run-Time Errors in Safety-Critical Software. - Darren Foulger; Steve King 001 (Ada-Europe, 2001)