26 entries tagged with #Code generation
by Jessie Glockner
Celebrating Women Engineering Heroes - International Women in Engineering Day 2021
Women make up roughly 38% of the global workforce, yet they constitute only 10–20% of the engineering workforce. In the U.S., numbers suggest that 40% of women who graduate with engineering degrees never enter the profession or eventually leave it. Why? The reasons vary but primarily involve socio-economic constraints on women in general, workplace inequities, and lack of support for work-life balance. Sadly, history itself has often failed to properly acknowledge the instrumental contributions of women inventors, scientists, and mathematicians who have helped solve some of our world's toughest challenges. How can young women emulate their successes if they don't even know about them?
by Simon Buist
Showing Global contracts with GNAT Studio
In the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated Global contracts inline with the code.by Roderick Chapman
Doubling the Performance of SPARKNaCl (again...)
Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack usage and code size at all optimization levels.by Roderick Chapman
Performance analysis and tuning of SPARKNaCl
This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.by Paul Butcher
Finding Vulnerabilities using Advanced Fuzz testing and AFLplusplus v3.0
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
by Juliana Silva
Make with Ada 2020: The autonomous firetruck
The AFT (Autonomous FireTruck) is a prototype of an autonomous firetruck that can put out fire without risking people's lives. This project won a finalist prize in the Make with Ada 2019/20 competition.by Emma Adby
Make with Ada 2020: Disaster Management with Smart Circuit Breaker
Shahariar's project ensures safety against electrical fire or shock during an earthquake, flood, gas leakage or fire breakout by disconnecting the mains with a smart circuit breaker. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.by Pierre-Marie de Rodat
A Further Expedition into Libadalang: Save Time with Libadalang.Helpers.App
Martyn’s recent blog post showed small programs based on Libadalang to find uses of access types in Ada sources. Albeit short, these programs need to take care of all the tedious logistics around processing Ada sources: find the files to work on, create a Libadalang analysis context, use it to read the source files, etc. Besides, they are not very convenient to run:
by Paul Butcher
AdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems
What's changed?In 2019 AdaCore created a UK business unit and embarked on a new and collaborative venture researching and developing advanced UK aerospace systems. This blog introduces the reader to ‘HICLASS’, describes our involvement and explains how participation in this project is aligned with AdaCore’s core values.
by Alexander Senier
RecordFlux: From Message Specifications to SPARK Code
Handling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset eases the creation of formally verified binary parsers in SPARK.by Arnaud Charlet
How Do We Use CodePeer at AdaCore
A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.
by Rob Tice
SPARKZumo Part 1: Ada and SPARK on Any Platform
So you want to use SPARK for your next microcontroller project? Great choice! All you need is an Ada 2012 ready compiler and the SPARK tools. But what happens when an Ada 2012 compiler isn’t available for your architecture?
by Yannick Moy
Tokeneer Fully Verified with SPARK 2014
Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran (Praxis at the time) in 2003 using the previous generation of SPARK language and tools, as part of a project commissioned by the NSA to investigate the rigorous development of critical software using formal methods. The project artefacts, including the source code, were released as open source in 2008. Tokeneer was widely recognized as a milestone in industrial formal verification. We recently transitioned this software to SPARK 2014, and it allowed us to go beyond what was possible with the previous SPARK technology. We have also shown how security vulnerabilities introduced in the code can be detected by formal verification.by Fabien Chouteau , Arnaud Charlet , Yannick Moy
SPARK Tetris on the Arduboy
One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.
by Quentin Ochem
Unity & Ada
Using Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.by Yannick Moy
Research Corner - SPARK 2014 vs Frama-C vs Why3
Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote with developers of the Why3 and Frama-C toolsets. In fact, it's a bloody good comparison really, that emphasizes the differences and benefits in each technology.by Yannick Moy
Research Corner - Proving Security of Binary Programs with SPARK
Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on proving security of binary programs. In this work, they use SPARK as intermediate language and GNATprove as proof tool, which is an atypical and interesting use of the SPARK technology.by Pierre-Marie de Rodat
C library bindings: GCC plugins to the rescue
I recently started working on an Ada binding for the excellent libuv C library. This library provides a convenient API to perform asynchronous I/O under an event loop, which is a popular way to develop server stacks. A central part of this API is its enumeration type for error codes: most functions use it. Hence, one of the first things I had to do was to bind the enumeration type for error codes. Believe it or not: this is harder than it first seems!
by Yannick Moy
Did SPARK 2014 Rethink Formal Methods?
David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington nuclear power plant and designed the specification method known as Parnas tables and the development method called Software Cost Reduction. In 2010, the magazine CACM asked him to identify what was preventing more widespread adoption of formal methods in industry, and in this article on Really Rethinking Formal Methods he listed 17 areas that needed rethinking. The same year, we started a project to recreate SPARK with new ideas and new technology, which lead to SPARK 2014 as it is today. Parnas's article influenced some critical design decisions. Six years later, it's interesting to see how the choices we made in SPARK 2014 address (or not) Parnas's concerns.by Yannick Moy
GNATprove Tips and Tricks: User Profiles
One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.by AdaCore Admin
AdaCore Tech Days 2015
by Raphaël Amiard
Make with Ada : From bits to music
I started out as an electronic musician, so one of my original motivations when I learnt programming was so that I could eventually *program* the sounds I wanted rather than just use already existing software to do it.
by AdaCore Admin
Project P Open Workshop
Project-P Open Workshop
by Yannick Moy
GNATprove Tips and Tricks: Minimizing Rework
As automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of techniques to ensure that, both for a single user, and when working in a team.by Olivier Ramonat
AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0
February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.