Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
Yannick Moy
AdaCore Tech Days Prez on SPARK
Yannick Moy
GNATprove Tips and Tricks: Catching Mistakes in Contracts
Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by…
Tristan Gingold
AdaCore at FOSDEM'15
Yannick Moy
GNATprove Tips and Tricks: Keeping Justifications Up-To-Date
GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications…
Lena Comar
ProofInUse is coming!
Yannick Moy
SPARK 2014 Rationale: Functional Update
While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently…
Emma Adby
A Busy Schedule Ahead!
Yannick Moy
SPARK 2014 Rationale: Object Oriented Programming
Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known…
Introducing the AdaCore Blog
We’re pleased to announce the launch of the AdaCore Blog providing an insight into the AdaCore Ecosystem.
Tristan Gingold, Yannick Moy
Tetris in SPARK on ARM Cortex M4
Cyrille Comar
Welcome To AdaCore's Blog
I'm proud, if not a bit nervous, to be the one firing the very first post on this brand new blog. Why are we starting a corporate blog at this time?…
Yannick Moy
SPARK 2014 Rationale: Ghost Code
A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the…