NVIDIA
NVIDIA: Adoption of SPARK Ushers in a New Era in Security-Critical Software Development
As one of the world's most trusted names in high-performance computing, security is essential to NVIDIA’s brand. With cybersecurity risks rising across the board, the company took an ambitious path to examine its software development methodology and find a more measurable solution. Ultimately, it chose to abandon C/C++ and adopt SPARK as its coding language of choice for verifying its most security-critical software and firmware components.
ITEC
Ada at ITEC: Real-Time Control over Complex Semiconductor Manufacturing Processes
Semiconductor manufacturing has some of the most exacting needs when it comes to performance and reliability, requiring millisecond-level precision and the ability to cost-effectively produce billions of smaller and smaller devices every year. That’s why ITEC, one of the major semiconductor manufacturing equipment and automation providers, chose Ada as its programming language to develop its critical control software.
IPESOFT
IPESOFT: Delivering reliable, long-lived energy and industrial systems with Ada and AdaCore
When IPESOFT was looking to develop its core real-time D2000 industrial automation platform, it knew that choosing the right development language and software tools would be crucial to the success of the platform and the company’s overall business growth. The solution needed to be reliable, secure, high performance, and easy and efficient to maintain over the long-term. Ultimately, IPESOFT chose AdaCore’s GNAT Pro and the Ada language to develop its D2000 platform.
LASP
Raising the Reliability of Scientific Space Exploration
How Ada is helping the Laboratory for Atmospheric and Space Physics minimize risk, reduce cost, and assure reliable control of software used for spacecraft and instrument operations.
Masten Space Systems
How Masten Space Systems is Using Ada and SPARK to Land on the Moon’s South Pole
To develop their mission-critical flight control software, Masten chose the Ada and SPARK programming languages, together with AdaCore’s GNAT Pro integrated development environment and the SPARK Pro static analysis tool suite for their XL-1 Lunar Lander. The lander will transport a suite of scientific research payloads to the lunar south pole.
Eldorado & Braile Biomédica
How Eldorado and Braile Biomédica Used AdaCore’s QGen Code Generator to Develop New Artificial Lung Equipment in Just Six Months
Eldorado used AdaCore’s QGen code generation and model verification tool suite on a cardiac pacemaker as a pilot project. Once they felt they had a mature understanding of how to use QGen in code generation and verification, they began applying QGen on other projects. One of those projects was Braile's new Solis System. With the partnership of Braile, the Eldorado Institute, and QGen, it was possible to complete a two-year development program in only six months.
SEAKR
How to Develop Reliable Spacecraft Systems at Lower Cost with the Ada Programming Language
When SEAKR Engineering decided to upgrade its mission-critical data recorder applications to a new hardware platform, they kept their software in Ada. To help them improve the efficiency and reliability of their Ada code, they upgraded their development environment to GNAT Pro.
Welch Allyn® devices — a Hillrom product family
Ada and SPARK: Beyond Static Analysis for Medical Devices
The need for safe and secure software — including Medical Device software — is becoming more important as cybersecurity threats in the healthcare sector become more frequent and severe. Hillrom migrated to Ada and SPARK to verify the safety of the code by formally proving some properties, and improving its efficiency by removing dynamic checks, all the while keeping development and verification costs down. Read the full case study to find out more.