The AdaCore Blog
An Insight Into the AdaCore Ecosystem
Information Hiding and Context Management in SPARK
Yannick Moy
Two Days Dedicated to Sound Static Analysis for Security
AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they…
Yannick Moy
Secure Software Architectures Based on Genode + SPARK
SPARK user Alexander Senier presented recently at BOB Konferenz in Germany their use of SPARK for building secure mobile architectures. What's nice…
Fabien Chouteau
Ada on the micro:bit
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…
Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2
This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing…
Yannick Moy
For All Properties, There Exists a Proof
With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to…
Johannes Kanig
Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto
Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 1
Pierre-Marie de Rodat, Yannick Moy, Fabien Chouteau, Raphaël Amiard
AdaCore at FOSDEM 2018
Lionel Matias
Leveraging Ada Run-Time Checks with Fuzz Testing in AFL
Fuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software…
Pierre-Marie de Rodat, Raphaël Amiard
Cross-referencing Ada with Libadalang
Manuel Iglesias Abbatermarco