you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html It also explains how to install GNATprove: ``alr…
and there are actually multiple ways to prove that the result is a permutation of the entry, either by computing a model multiset (a.k.a. bag) of the value on entry and exit and showing they are equal, or by exhibiting…
For a related eye-opening result, with both practical application and interesting research backing it, see this talk on "Quicksorts of the 21st century" at Newton Institute on Verified Software last year:…
You can get automatic resource handling with controlled types, but this is not part of the baremetal minimal runtime you can use for a driver. You can get ownership tracking with SPARK, but you need to use proof…
Here, we are targeting full functional specification, which is hard. So there is a lot of ghost code to support the proof (the loop invariants, assertions and ghost entities). That's what's driving the verification time…
I confirm that we're following closely what Xavier is doing for Rust, and even copied his work on "prophecy variables" to take the effects of borrowing into account in loop invariants in SPARK! Your plans for having…
As someone said, the best solution here is to use the dimensionality analysis in GNAT: https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ug... as in: with Ada.Text_IO; use Ada.Text_IO; with System.Dim.Float_Mks;…
It has changed: https://blog.adacore.com/pointer-based-data-structures-in-sp...
You can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"):…
We have a compiler from a subset of Ada & SPARK to C: http://docs.adacore.com/live/wave/gnat_ccg/html/gnatccg_ug/g... But that's not the same as having a full certified (in the sense of Coq) compiler. If we were to use…
Funny that you pointed to the workshop at KAIST. My colleague Johannes Kanig presented SPARK there, he's on the front row with a SPARK t-shirt. :-) Regarding your Brute-Force Assurance Concept, it connects to the…
Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they…
I would be interested in your repository of resources, is it something you plan to make public soon? Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification,…
you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html It also explains how to install GNATprove: ``alr…
and there are actually multiple ways to prove that the result is a permutation of the entry, either by computing a model multiset (a.k.a. bag) of the value on entry and exit and showing they are equal, or by exhibiting…
For a related eye-opening result, with both practical application and interesting research backing it, see this talk on "Quicksorts of the 21st century" at Newton Institute on Verified Software last year:…
You can get automatic resource handling with controlled types, but this is not part of the baremetal minimal runtime you can use for a driver. You can get ownership tracking with SPARK, but you need to use proof…
Here, we are targeting full functional specification, which is hard. So there is a lot of ghost code to support the proof (the loop invariants, assertions and ghost entities). That's what's driving the verification time…
I confirm that we're following closely what Xavier is doing for Rust, and even copied his work on "prophecy variables" to take the effects of borrowing into account in loop invariants in SPARK! Your plans for having…
As someone said, the best solution here is to use the dimensionality analysis in GNAT: https://docs.adacore.com/gnat_ugn-docs/html/gnat_ugn/gnat_ug... as in: with Ada.Text_IO; use Ada.Text_IO; with System.Dim.Float_Mks;…
It has changed: https://blog.adacore.com/pointer-based-data-structures-in-sp...
You can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"):…
We have a compiler from a subset of Ada & SPARK to C: http://docs.adacore.com/live/wave/gnat_ccg/html/gnatccg_ug/g... But that's not the same as having a full certified (in the sense of Coq) compiler. If we were to use…
Funny that you pointed to the workshop at KAIST. My colleague Johannes Kanig presented SPARK there, he's on the front row with a SPARK t-shirt. :-) Regarding your Brute-Force Assurance Concept, it connects to the…
Thanks for the links to interesting articles. Definitely interested in the interior point formalization and proof. As I expected, it's already quite hard even without taking floats into account. (In the conclusion they…
I would be interested in your repository of resources, is it something you plan to make public soon? Something I find very useful as a developer is to see how tools work on concrete examples. For formal verification,…