Articles Tagged “GNATprove”
3 articles tagged “GNATprove”, newest first.
-
Proving Image Processing Free of Out-of-Bounds Access with SPARK — Binarization, Smoothing, Labeling and a Speed Comparison with C
Proving with SPARK's GNATprove that image-processing code never reads or writes outside the image, using binarization, 3×3 smoothing and labeling: how to wri...
-
Starting an Ada Project with Alire — Creating a Project, Adding Dependencies, Build Profiles, and GNATprove
Using Alire, the Ada package manager, to create a project, fetch GNAT automatically, add crates, switch build profiles, and prove code with GNATprove, with r...
-
Introduction to Formal Verification with SPARK — From Ada Contracts to Mathematical Proof
A practical introduction to formal verification using the SPARK subset of Ada. Covers how to step up from contracts (Pre/Post) to proofs, using GNATprove, lo...