en de fr

AdaCore Releases SPARK Pro 16

Formal verification toolset helps reduce certification effort for safety-critical and high-security systems

ERTS2 2016, Toulouse, France, January 27, 2016 - AdaCore today announced the latest release of its SPARK Pro integrated development and verification environment, bringing a sound and mathematics-based static analysis technology to the challenges of software verification for high-assurance systems. SPARK Pro 16 provides enhanced coverage of SPARK 2014 language features and now supports the Ravenscar tasking profile, thus extending the benefits of formal verification methods to a safe subset of Ada 2012 concurrent programming features. As another improvement SPARK Pro 16 can generate counterexamples to verification conditions that cannot be proved, thus making it easier for developers to find defects in the functional code or in the supplied contracts. SPARK Pro 16 also improves the handling of bitwise (modular) operations, and the product’s proof engine now includes the Z3 SMT solver.

The SPARK Pro technology, which has been jointly developed by AdaCore and its partner Altran, can prove SPARK program properties ranging from absence of run-time errors (exceptions) to compliance with a formally defined requirements specification. SPARK Pro thereby helps reduce the cost of software verification and simplifies the task of certifying the software against safety or security standards. The technology is sound; that is, there are no “false negatives”: if SPARK Pro reports that a program is free of a certain kind of error, then that error cannot occur. It also has a very low “false positive” rate, which is important in practice, and its efficient SMT solver technology scales up for usage in large projects. The SPARK language and toolset can be used from the outset on new projects or introduced incrementally into an existing project, allowing a “hybrid” verification approach that combines formal methods with traditional testing techniques.

“With this new version of the SPARK Pro toolset, we get one step closer to our goal: to make it easy for software engineers to start relying heavily on static verification and formal proofs without needing expertise in mathematical logic,” said Cyrille Comar, AdaCore President. “Not only are most of the needed proofs conducted completely automatically, but many language restrictions usually associated with such proof capabilities have been lifted. This makes the writing of proven software both efficient and pleasant”.

About SPARK Pro
SPARK Pro provides the foremost language, toolset, and design discipline for engineering high-assurance software. It combines the SPARK language and verification tools with AdaCore’s GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments.

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, which can then be used to meet the requirements of safety and security certification schemes, such as DO-178B and DO-178C (airborne systems), EN 50128 (railway systems), and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C.

About SPARK 2014
SPARK 2014 is a formally analyzable programming language especially suited for developing ultra-low defect software in critical applications, for example where safety and/or security are key requirements. The SPARK language has a solid industrial track record with a 25+ year history of successful usage worldwide in a range of industrial applications including civil and military avionics, railway signaling, cryptography, and cross-domain solutions. SPARK 2014 is the next generation of this leading software technology, offering key benefits such as support for hybrid verification (combining formal methods with traditional testing), executable contracts, a larger Ada language subset (for example including generic units), and convergence with Ada 2012 syntax (making it easier to combine Ada and SPARK components). An on-line interactive course on SPARK 2014, part of the AdaCore University curriculum, is available at http://university.adacore.com/courses/spark-2014/.

Availability
SPARK Pro 16 is available now. For more information please contact info@adacore.com, and for a demo please visit www.adacore.com/sparkpro/demos

About AdaCore
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems. Four flagship products highlight the company’s offerings:

  • The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
  • The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software,
  • The SPARK Pro verification environment, a toolset based on formal methods and oriented towards high-assurance systems, and
  • The QGen model-based development tool, a qualifiable and customizable code generator and verifier for Simulink® and Stateflow® models, intended for safety-critical control systems.

Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, rail systems, medical devices, and financial services. AdaCore has an extensive and growing world-wide customer base; see www.adacore.com/customers/ for further information.

AdaCore products are open source and come with expert on-line support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts
Jamie Ayre
AdaCore
press@adacore.com
http://twitter.com/AdaCoreCompany

Jenna Beaucage
Rainier Communications (for AdaCore)
Tel: +1-508-475-0025 x124
jbeaucage@rainierco.com