Libre News
Open Source SPARK Implementation of Skein Algorithm
Altran Praxis and AdaCore have released a new reference implementation of the Skein algorithm, written and verified using the GPL 2010 Edition of the SPARK language and toolset. Skein is a cryptographic hash function and an entrant in the National Institute of Standards and Technology (NIST) hash function competition to design what will become the new Secure Hash Algorithm (SHA-3) standard. Such hash functions are used to compute short “digests” of long messages, and are one of the key building blocks of digital communication and cryptographic systems.
SPARK GPL 2010 now available!
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 Praxis with the GNAT Programming Studio (GPS) and GNATBench development environments from AdaCore.
GNAT GPL 2010 now available!
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.
Hi-Lite project officially launched
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 Praxis, 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 hi-lite-discuss@lists.forge.open-do.org.
Event: Ada and SPARK for Education and Research
Tuesday Feb 23 2010, Heverlee, Belgium
This event is primarily intended for the educational and research community, and will present experts from academia and industry who believe that using Ada and SPARK in education and research is fundamental to form the software engineers of tomorrow. Why Ada? Because they believe that Ada is the right choice for a range of courses including elementary programming, data structures, software engineering and for more advanced courses and research in compiler construction, real-time systems, robotics, cryptography, etc. Ada and SPARK embody the best contemporary ideas in software technology, and students exposed to these languages at an early stage of their career become more skilled and principled programmers.
Webinar: Introducing CodePeer
Tuesday, March 9, 5:00pm CET / 11:00 am EST / 8:00 am PST
Recently launched, CodePeer is a source code analyzer that detects run-time and logic errors in Ada programs. Serving as an efficient and accurate code reviewer – in effect an expert assistant. CodePeer identifies constructs that are likely to lead to run-time errors such as buffer overflows, and it flags legal but suspect code typical of logic errors. Going well beyond the capabilities of typical static analysis tools, CodePeer also produces a detailed analysis of each subprogram, including pre- and postconditions. This webinar will describe and demo some of the features of CodePeer and allow you to ask questions directly to the designers of the tool.
Find the bug challenge
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.
Ada Powers Dasher, The Running Robot
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.
Open-Do Conference – Combining Formality with Agility for Critical Software Development
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.
GNAT Pro Insider newsletter available
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.
The Open-DO Qualifying Machine
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.
Praxis and AdaCore Launch SPARK GPL
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.
Tokeneer Discovery Tutorial Now Available
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.
Open-DO forge Launched
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.
GNAT GPL Edition for the LEGO MINDSTORMS NXT
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 Tokeneer Project
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.
The Lean, Agile Approach to High-Integrity Software
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!
Project Coverage Launch
Thanks to French public funds, the next generation of Free Software code coverage tools is on its way. “Project Coverage” will produce a Free Software coverage analysis toolset together with the ability to generate artifacts that allow the tools to be used for safety-critical software projects undergoing a DO-178B software audit process for all levels of criticality