This article series is in the TechXchange: Developing High Quality Software
Ada a general purpose programming language that incorporates advanced programming features like contracts and object oriented programming support.
SPARK is a subset of the latest version of Ada that can be formally proven to be free of bugs. It takes advantage of Ada 2012’s contract support.
We have collected articles that are related to Ada and SPARK here.
Ada and SPARK Basics
- 11 Myths About Ada
- What's The Difference: Ada Then and Now
- What’s the Difference Between Ada and SPARK?
- C++11 and Ada 2012 - renaissance of native languages?
Enforced Coding Using Ada Contracts
- Ada 2012: The Joy of Contracts
- Contract-Driven Programming Takes Specification Beyond The Stone Age
- Use Contracts To Enforce Effective Coding
- Q&A: Formal Methods Push Toward Zero-Defect Software
- Requiem for a Bug – Verifying Software: Testing and Static Analysis
- Requiem for a Bug – Verifying Software, Part 2: Formal Verification through SPARK 2014
Using Ada and SPARK
- Helpful Hints for Adopting SPARK
- Ada and RISC-V Secure Nvidia’s Future
- Use Ada for Your Web Development
Ada, SPARK and Other Languages
- Comparing Ada and C
- What’s the Difference Between SPARK 2014 and Apache Spark?
- Rust and SPARK: Software Reliability for Everyone
- C Programmers, Time To Try Ada
- Ada Offers Advantages Over C And C++
High Reliability Software
- Q&A: Formal Methods Push Toward Zero-Defect Software
- Rust and SPARK: Software Reliability for Everyone
- Addressing the Growing Complexity of Embedded Systems
- Are You Writing Safe And Secure Software?
Reducing Costs Using Ada
- Ada—The Language of Cost Savings?
- GNAT Pro Developer Cuts Ada, SPARK Development Costs
- Leveraging SPARK and Ada in Cutting-Edge Auto Systems
Learning Ada and SPARK
Make with Ada Competition
- The Many Ways You Can “Make with Ada”
- Make with Ada 2019
- They Made It with Ada and SPARK
- Are You Up for the Ada Challenge?