8 entries tagged with #tooling
by Yannick Moy , Claire Dross
Proving the Correctness of GNAT Light Runtime LibraryThe GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use at the highest levels of criticality in several industrial domains. It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations. We have used SPARK to prove the correctness of 40 of them: that the code is free of runtime errors, and that it satisfies its functional specifications.
by Léo Germond
How To: GNAT Pro with Docker
Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!
GNAT Community 2019 is here!
We are pleased to announce that GNAT Community 2019 has been released! See https://www.adacore.com/download.
Taking on a Challenge in SPARK
Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.