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 email@example.com.
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 Apr 23, 2013
- Tuesday Apr 23, 2013
- Tuesday Apr 23, 2013
- Tuesday Feb 26, 2013
- Tuesday Feb 26, 2013