Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
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…
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…
Emma Adby
Introducing the Make With Ada competition!
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…
Pierre-Marie de Rodat