Viewing profile — yannickmoy

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 ex…

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 sh…

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 Veri…

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 S…

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…

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 invaria…

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 …

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"): https://blog…

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 sen…

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 Assur…

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…

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 concret…