Content by M. Anthony Aiello
M. Anthony Aiello
Tony Aiello is a Product Manager at AdaCore. Currently, he manages SPARK Pro, GNAT Pro for Rust, and GNAT IQ.
Challenging Agentic AI with SPARK using OpenUxAS
“How well does generative AI do with writing Ada?” The simple answer is: “quite well!” But the details are also interesting, so I encourage you to…
GNAT IQ
AdaCore is delighted to announce unlimited access to GNAT IQ, AdaCore’s AI-powered GNAT documentation chatbot, for all of our current customers.
Revisiting the Mars Rover Safety Monitor
In the blog "Let's Write a Safety Monitor for a Mars Rover", I made a big assumption in the procedure that moves that Rover forward; here, I relax…
Introduction to Formal Verification with SPARK
Let’s Write a Safety Monitor for a Mars Rover!
The Ada Mars Rover shouldn’t crash into obstacles. See how we formalized this property, discovered an unstated assumption in our remote-control mode…
Proving Software Security with SPARK Pro
Co-Developing Programs and Their Proof of Correctness
I am delighted to announce that the Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of…
Memory Safety with Formal Proof
GNAT Static Analysis Suite: A Vision for Static Analysis in Ada
You may have noticed that over the past two years, we have made significant updates to our CodePeer product - the most visible change being the…
