GNAT and SPARK GPL 2016 released!
We are pleased to announce the availability of the GNAT and SPARK GPL 2016 toolsets.
GNAT GPL 2016 incorporates upgraded technology for the debugger (GDB 7.10) along with support for the Windows 10 platform and many new features.
Ada runtime support has been extended for the STM32f429-disco, STM32f469-disco and STM32F7-disco development boards based on the STM32 family of microcontrollers.
- ravenscar sfp/full for the stm32f429-disco board
- ravenscar sfp/full for the stm32f469-disco board
- ravenscar sfp/full for the stm32f7-disco board
SPARK GPL 2016 - the formal method verification toolset - includes the following new features:
- Support for concurrency with Ravenscar and type predicates
- Generation of counterexamples for unproved checks
- Better support of bitwise (modular) operations in proof
- Generation of global summary table
You will find documentation about the GNAT GPL 2016 and SPARK GPL 2016 toolset here:
AdaCore Introduces GNAT GPL 2015 for the Raspberry Pi 2
Latest version of AdaCore cross-development environment targets students and other developers of nonproprietary software
NEW YORK and PARIS, Sep 1, 2015 – AdaCore, the leading provider of commercial software solutions for the Ada programming language, today released a freely downloadable version of its GNAT GPL Ada cross-development environment for the Raspberry Pi 2 micro-PC running Embedded Linux. With this new cross-development environment, professors, students, hobbyists and others can take advantage of Ada 2012’s reliability, safety and security benefits for their Raspberry Pi 2 applications.
"Raspberry Pi 2 Model B v1.1 top new (bg cut out)" by Multicherry. Licensed under CC BY-SA 4.0 via Commons - https://commons.wikimedia.org/wiki/File:Raspberry_Pi_2_Model_B_v1.1_top_new_(bg_cut_out).jpg
GNAT GPL provides a complete Ada 2012 development environment, including a comprehensive tool-chain as well as AdaCore’s flagship GNAT Programming Studio (GPS) Integrated Development Environment (IDE). GNAT GPL implements the Ada 2012 language standard by default, which includes these important language features:
- Contract-based programming (preconditions, post-conditions, and type invariants) including support for the Liskov Substitution Principle in Object-Oriented Programming
- More general expressions (conditional expressions, quantified expressions, expression functions)
- Enhanced multiprocessor support (multiprocessor affinity and barriers)
- Enhanced integration of concurrency and OOP
- Additional language-defined libraries (vector/matrix libraries)
“With more than 5 million units sold to date, Raspberry Pi is one of the world’s most popular single-board computers for young computer innovators and hobbyists,” said Jamie Ayre, Marketing Director of AdaCore. “By providing Raspberry Pi 2 users access to the very robust, high-integrity development environment of Ada, we’re opening the door to some really creative solutions and the next generation of Ada programmers.”
With the release of GNAT GPL for Bare Board ARM in 2014, an implementation on the Raspberry Pi 2 running Linux on ARM was a natural follow-up. It reflects AdaCore’s ongoing commitment to the Ada community to provide freely available Ada implementations for developers of nonproprietary software. Fully featured releases of this GNAT technology are also available for GNU Linux, Mac OS X, Bare Board ARM, and Windows.
About Raspberry Pi 2
The Raspberry Pi 2 Model B is the second generation Raspberry Pi, released in February 2015. The 900MHz quad-core ARM Cortex-A7 CPU increases the performance almost 6 times, and the 1GB LPDDR2 SDRAM accommodates larger and faster systems. The Raspberry Pi 2 Model B retains the various interfaces of its predecessor, such as 4 USB ports, 40 GPIO pins, a full HDMI port, and an Ethernet port. With its low cost / high performance advantages, the Raspberry Pi 2 is an attractive choice in many kinds of systems including Internet of Things (IoT) applications.
About AdaCore [JA1]
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 worldwide customer base; see www.adacore.com/customers/ for further information.
508.475.0025, ext. 124
Announcing the immediate availability of GNAT and SPARK GPL 2015
We are pleased to announce the availability of the GNAT and SPARK GPL 2015 toolsets.
GNAT GPL 2015 includes support for the Raspberry Pi 2 allowing Ada development using all Ada features on this popular educational computer running embedded Linux.
GNAT GPL 2015 incorporates upgraded technology for the back end (GCC 4.9) and debugger (GDB 7.8) and many new features, including the following:
- Improved diagnostic messages
- Fine-grained control over the treatment of warnings
- Extended support for non-default endianness
- Support for large files on 32-bit systems
- Improved handling of inlining
- Overflow checks enabled by default
- Enhanced code generation and debugging capabilities
- Support for aggregate projects in all tools
- Support for stubbing of units in GNATtest
It also comes with the latest version of the GPS IDE, GPS 6.1.1. that includes better support for Ada 2012 and SPARK 2014 and a simplified workflow and project templates for bare board platforms.
GPL editions of GNATbench, AJIS, and PolyORB will be released at a later date.
SPARK GPL 2015 - the formal method verification toolset - includes a number of major enhancements. New language features include in particular support for Object-Oriented programming and "ghost code" used for proof only, with no impact on the generated code.
Proof capability has been significantly improved with the integration of two provers by default (Alt-Ergo and CVC4), additional automatic generation of contracts, more precise analysis of modular (bitwise) operations, and improved support for manual provers.
Usability has also been enhanced through better categorization of messages and output of assumptions made for each verification result.
SPARK GPL 2015 also ships with additional examples, in particular a standalone TCP/IP stack implementation.
This document will present the Ada language using terminology and examples that are familiar to developers that understand the C++ or Java languages.
To download the booklet, please visit this page
We are pleased to announce the availability of GNAT GPL 2013 and SPARK Hi-Lite GPL. GNAT GPL 2013 provides new Ada 2012 language features, introduces new tools and new versions of existing tools, incorporates a range of improvements and adds several new platforms.
SPARK Hi-Lite GPL 2013 is a package that can be installed after GNAT GPL 2013, to provide access to the new SPARK toolset that was developed in project Hi-Lite. This release is a major evolution of the SPARK toolset providing formal verification for a subset of Ada programs. This new toolset uses Ada 2012-style contracts (e.g. pre- and postconditions), instead of the stylized comments in previous versions, to provide specifications of programs.
A preview of the data and information analysis is also available. For more information on SPARK 2014, please visit www.spark-2014.com.
Dr. Martin C. Carlisle, the director of the Academy Center for Cyberspace Research at the United States Air Force Academy has developed a secure DNS server using Ada and the SPARK formal methods tool set.
We are pleased to announce the release of GNAT GPL 2012, the integrated Ada, C, C++ toolset for for Academic users and FLOSS developers. This new edition provides many new features and enhancements in all areas of the technology.
SPARK GPL 2012 provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Altran with the GNAT Programming Studio (GPS) and GNATBench development environments from AdaCore.
We are pleased to announce the release of Ada 2012 and the official launch of the Ada 2012 website. Ada 2012 is the next generation and this new addition provides many new features and enhancements. Explore the new site and learn the new features and benefits of Ada.
If you couldn’t make it to this year’s Ada Connection event in Edinburgh, we will be posting a selection of the recorded talks.
We are pleased to announce the release of GNAT GPL 2011, the integrated Ada, C, C++ toolset for for Academic users and FLOSS developers. This new edition provides many new features and enhancements in all areas of the technology.
The first in a series of 5 SPARK Pro demos that will present a practical, hands-on introduction on using the most important features of the SPARK programming language has been published.
Ada-Europe Kicks Off its First Annual Student Programming Contest “The Ada Way”
Brussels, Belgium (September 28, 2010) – Ada-Europe, the international organization that promotes the knowledge and use of the Ada programming language in European academia, research and industry, is pleased to announce “The Ada Way“. This annual student programming contest aims to attract students and educators to Ada in a form that is both fun and instructive. Entries are now open for the 2010-11 competition and judging takes place in May next year.
In line with the start of the football season, this year’s challenge is to build a software simulator of a football match. The software system, programmed in Ada, will need to support a number of gaming and football features including speed, tactical skills and player fatigue. The submitted code will include a software core, implementing the logic of the simulation, as well as read-write graphical panels for participating football team managers.
Candidate submissions will be judged on a number of evaluation criteria including:
- Coverage of requirements
- Syntactic, semantic, programmatic and design correctness
- Clarity and readability of the code
- Quality of design
- Availability for the LEGO MINDSTORMS robotic building system
- Ingenuity and cuteness of the solution
- Time and space efficiency of the solution
The winning submission will win a framed award, one free registration and up to 3 reduced student fees for representatives of the winning team to attend to the Ada-Europe 2011 Conference, accommodation and airfare for the team representatives, an exhibition slot in the conference program, and visibility in electronic and printed media. This year’s competition is sponsored by Ada-Europe, AdaCore, and Atego.
To enter, and for the full specification and details of software requirements, please go to the official web site of “The Ada Way”, www.ada-europe.org/AdaWay.
Ada-Europe is the international non-profit organization that promotes the knowledge and use of the Ada programming language in academia, research and industry in Europe. Ada-Europe has member organizations all over the continent, in Belgium, Denmark, France, Germany, Spain, Sweden, Switzerland, as well as individual members in many other countries.
A PDF version of this press release is available at www.ada-europe.org.
Dirk Craeynest, Ada-Europe Vice-President, Dirk.Craeynest@cs.kuleuven.be
SPARK GPL 2010 provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Altran with the GNAT Programming Studio (GPS) and GNATBench development environments from AdaCore.
We are pleased to announce the release of GNAT GPL 2010, the integrated Ada,C,C++ toolset for for Academic users and FLOSS developers. This new edition provides many new features and enhancements in all areas of the technology.
Yesterday saw the official launch of the Hi-Lite project. Financially supported by French national and local government agencies, Hi-Lite aims to increase the use of formal methods in developing high integrity software, particularly to meet the forthcoming DO-178C avionics standard.
Hi-Lite is completely based on libre software. The project is structured in two different toolchains for Ada and C based on GNAT/GCC compilers, the SPARK verification toolset and the Frama-C platform. The integration of these toolchains inside two industrial IDEs offers to the user a common interaction on Ada and C programs. In particular, mixed Ada/C programs can be verified against a common specification.
The project partners are AdaCore, Altran, Astrium Space Transportation, CEA-LIST, the ProVal team of INRIA and Thales Communications. AdaCore is the project leader. For more information please visit www.open-do.org/projects/hi-lite and to subscribe to the public mailing list please send email to firstname.lastname@example.org.
In order to demonstrate the scope of recently launched CodePeer’s code analysis capabilities we thought we’d have a little fun and each month post a simple piece of code that contains a few tricky bugs, so that you can measure your bug-finding capacities to those of CodePeer.
Learn how Prof. Lars Asplund, and a team of 21 students created Dasher, a human sized robot designed to run using its own locomotion and balance. Behind it all is AdaCore’s GNAT Ada toolsuite.
The Fall/winter newsletter is now online. This edition features stories on our GNAT Pro High-Integrity Edition for MILS, the Model-Based Design projects that are currently underway as well as the usual info on releases, academia, webinars, and all things related to GNAT.
This conference brings together experts from the two fields and asks the question “Can Formality and Agility be combined?” to develop software that has to reach the highest levels of safety and security.
A Qualifying Machine (QM) is an agile and lean infrastructure to ease DO-178 tool qualification. The main goal of a QM is to ease the manipulation of all artifacts within the whole application life cycle and to track the activities performed by the development team.
Within Open-DO, we released an instantiation of the QM concept for GNATcheck, a coding standard checking tool qualifiable for DO-178. The infrastructure and qualification material (including the Tool Qualification Plan and the testing framework) are freely available as open source in the Open-DO forge. With this initiative, we intend to promote open collaborations in the high-assurance domain and to show how to deploy a lean and agile qualification process.
The launch of a new, General Public License (GPL) version of SPARK brings a professional-grade toolset for high-assurance and safety-critical software development to the academic community and developers of Free Software. This aims to drive the use of high assurance programming techniques and tools by a larger percentage of the overall software development community.
Over the summer the Open-DO team has been busy working on putting in place the Open-DO Forge (collaborative platform) that will host all the current projects being developed.
Explore this tutorial that provides an introduction to the SPARK programming language and Toolset for engineering high-assurance software using the source code from the Tokeneer Project. It contains a series of lessons that demonstrates key features of the language and Toolset, illustrating why SPARK is superior to other standard imperative languages for building high-assurance software. SPARK also prevents the occurrence of a number of the top twenty-five most dangerous programming errors.
A hands on look at an NSA funded, highly-secure biometric software system. Download the sources and tools used to develop the Tokeneer System (a biometric reader) and learn first hand how to develop highly secure software systems.
GNAT GPL Edition for the LEGO MINDSTORMS NXT platform brings the possibility of experimenting with embedded systems development using the Ada 2005 and SPARK languages to an education-oriented robotic platform.
The “Lean, Agile Approach to High-Integrity Software” event took place on March 26 at the Maison de la Chimie in Paris. In all, over 80 people joined us for a day dedicated to looking at ways in which Lean and Agile methods can (and are!) being used to develop software that requires certification – a very heavy process as many of you will know. The videos and slides from the workshop will be posted at a rate of 1 per week starting next week. Thanks to everyone that participated and made the day so valuable!
- Tuesday Mar 21, 2017
- Tuesday Mar 21, 2017
- Tuesday Mar 14, 2017
- Tuesday Mar 14, 2017
- Tuesday Dec 6, 2016