Ada Resource Association

Stuart Matthews explains how SPARK 2014 uses and extends the features of Ada 2012 for automated verification of programs.

This two-part article discusses the benefits of developing code with automated static analysis, and then shows examples of doing so, using SPARK.

The industrialization age of programming by contract is opening a new era in software development. Just as development techniques went from assembly to structured languages and from structured languages to object orientation, contract-based programming is providing one more abstraction to software design.

Professors and students at Vermont Technical College are using AdaCore’s GNAT Ada development environment and Altran Praxis’ SPARK tools to implement two NASA-sponsored programs, including a CubeSat.

Static and dynamic code analysis can improve application performance, safety and reliability by identifying problems early in the development cycle if the proper tools and procedures are used from the start. Dr. Mike Hennell, founder of LDRA, spoke with me about the various aspects of these types of tools.

Altran Praxis announced that its SPARK language has been selected by a new, NASA-funded US lunar mission. SPARK will be used to develop the software behind a CubeSat project being developed by a consortium comprising Vermont Technical College, Norwich University, St. Michael’s College, and the University of Vermont.

An article in GCN (Government Computing News) that looks at an NSA-funded project carried out by the U.K.-based Praxis High Integrity Systems and Spre Inc. NSA commissioned the project, which involved writing code for an access control system, to demonstrate high-assurance software engineering.

In this article by David Norfolk and Pan Pantziarka, the authors look at the increasing use of Formal Methods and the Correctness by Construction process championed by Altran Praxis.