Blog
An Insight Into the AdaCore Ecosystem
Proving Safety at Scale: SPARK, RISC-V, and NVIDIA’s Security Strategy
Read More
Yannick Moy
Research Corner - SPARK on Lunar IceCube Micro Satellite
Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar…
Piotr Trojanek
Verifying Tasking in Extended, Relaxed Style
Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs…
Olivier Ramonat
Simplifying our product versioning
Looking at the list of product versions that were expected for 2017 it became clear that we had to review the way we were handling product versioning.
Claire Dross
SPARK 2014 Rationale: Support for Type Invariants
Type invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation.…
Emmanuel Briot
GNAT On macOS Sierra
GNAT and all the tools work great on the newly released macOS Sierra, but gdb needs some tweaking of the system.
Yannick Moy
Verified, Trustworthy Code with SPARK and Frama-C
Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified,…
Emmanuel Briot
Debugger improvements in GPS 17
The GNAT Programming Studio support for the debugger has been enhanced. This post describes the various changes you can expect in this year's new…
Yannick Moy
The Most Obscure Arithmetic Run-Time Error Contest
Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course,…
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.…
Emmanuel Briot
GNAT Programming Studio (GPS) on GitHub
The GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.
Emmanuel Briot
Bookmarks in the GNAT Programming Studio (GPS)
As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view,…
Claire Dross
Automatic Generation of Frame Conditions for Record Components
Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the…