Tony Aiello is SPARK Pro Product Manager, RecordFlux Product Manager, and GNAT Pro for Rust Product Manager at AdaCore.
2 entries written by Anthony Aiello
The Ada Mars Rover shouldn’t crash into obstacles. See how we formalized this property, discovered an unstated assumption in our remote-control mode that could have led the Rover to crash, removed the assumption, and ultimately proved this property using SPARK. You’ll be surprised how little new code - including proof code - was needed!
I am delighted to announce that the Communications of the ACM has published a paper on SPARK: “Co-Developing Programs and Their Proof of Correctness”. The paper provides a comprehensive and up-to-date presentation of SPARK; as such, it’s a great reference to share with anyone - in industry, academia, or anywhere in between - who might like to know more about SPARK.