BATH, NEW YORK and PARIS, November 29, 2012 – High Assurance Software Symposium and SPARK User Group – AdaCore and Altran Praxis today announced the release of the SPARK Pro 11 software development and verification environment, providing a major step forward for the developers of high-assurance systems. SPARK Pro 11 offers many enhancements particularly in the area of program proof.
Major improvements to proof functions
A number of significant enhancements have been made to the way that functions and proof functions are handled in SPARK Pro 11. These changes will improve project efficiency by eliminating the vast majority of rules that were previously manually encoded. The main changes include a more powerful language for specifying proof functions and the ability to use the functions in any proof context. This greatly simplifies the task of writing and maintaining functional contracts for critical software, providing high-assurance at lower cost.
Counter-example generation
Proof is a very powerful technique for achieving high levels of assurance in safety or security-critical software. However, when performing proofs users typically spend much of their time inspecting undischarged “verification conditions” to determine whether they can indeed be proved. Included with SPARK Pro 11, Riposte is a new tool that not only determines whether a verification condition is false, but can also generate a counter-example to demonstrate the conditions under which it is false. Riposte is a major improvement to the verification workflow, saving projects a significant amount of time previously spent analyzing unprovable verification conditions and providing developers with intuitive explanations. Riposte was developed jointly by Altran Praxis and the University of Bath (UK).
Clearly defined assumptions
The new assume contract in SPARK Pro 11 allows users to introduce system-level assumptions about programs into their proofs in a clear and concise format. Previously, these assumptions might have been captured by user rules or manual review.
About SPARK Pro
SPARK Pro, a product jointly developed by Altran Praxis and AdaCore, provides the foremost language, toolset and design discipline for engineering high-assurance software. It combines Altran Praxis’ acclaimed SPARK language and verification tools, with the GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments from AdaCore. There are SPARK versions based on Ada 83, Ada 95, and Ada 2005, so all standard Ada compilers and tools work out-of-the-box with SPARK.
SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness, including proofs of the absence of run-time errors that can be used to meet the requirements of safety and security certification schemes, such as DO-178B, DO-178C, and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C
Availability
SPARK Pro 11 is available now. For more information please visit http://www.adacore.com/home/products/sparkpro/ or contactinfo@adacore.com.
Demonstration
A demonstration providing an introduction to the new features in SPARK Pro 11 is available now at http://adaco.re/2h.
About Altran Praxis
Altran Praxis is a specialist systems and software house, focused on the engineering of systems with demanding safety, security or innovation requirements. Altran Praxis leads the world in specific areas of advanced systems engineering and innovation such as: ultra-low defect software engineering, Human Machine Interface (HMI), safety engineering for complex or novel systems, systems engineering and methods/tools (such as SPARK). Altran Praxis offers clients a range of services including turnkey systems development, consultancy, training and R&D. Key market sectors are aerospace and defense, rail, nuclear, air traffic management, automotive, medical and security. The company operates globally with active projects in the US, Asia and Europe.
Altran Praxis is a wholly owned subsidiary of the Altran Group (altran.com) — a global leader in innovation and high-tech engineering consulting with a global network of 17,000 collaborators (including 15,000 consultants) and 500 major clients throughout the world. www.altran-praxis.com
About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore’s flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see http://www.adacore.com/home/company/customers/ for further information.
Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railway systems and medical devices, and in security-sensitive domains such as financial services.
AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com
