Modern cybersystems need to be reliable, safe and secure. At AdaCore we see Ada and its formally verifiable subset SPARK as key technologies for enabling embedded systems developers to meet these requirements.
The Ada programming language encourages a ‘think first, code later’ discipline that helps produce more readable, reliable and maintainable software. AdaCore personnel have been actively involved with the Ada language effort since its inception, and the company’s flagship GNAT technology implements all versions of the language standard, including the Ada 2012 revision.
The SPARK language is an Ada subset that supports formal verification, which is especially useful for high assurance applications where absence of run-time errors needs to be demonstrated with mathematical rigor. AdaCore has been actively involved with the evolution of the SPARK language, and the company’s SPARK toolset implements the latest version of the language, SPARK 2014.
AdaCore created the Make with Ada competition specifically to promote the use of the Ada and SPARK languages and demonstrate their advantages. Our hope is that by participating in this competition individuals, or small teams, will gain first-hand experience with these technologies and their benefits.