yannickmoy

5 ms·

1. 1.▲
   by yannickmoy 4y ago

   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 with
2. 2.▲
   by yannickmoy 4y ago

   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 the permutation to ap
3. 3.▲
   by yannickmoy 4y ago

   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: https://www.ne
4. 4.▲
   by yannickmoy 4y ago

   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 techniques. There are pointe
5. 5.▲
   by yannickmoy 5y ago

   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 up. I don&
6. 6.▲
   by yannickmoy 5y ago

   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 Rust anal
7. 7.▲
   by yannickmoy 6y ago

   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 Syst
8. 8.▲
   by yannickmoy 7y ago

   It has changed: https://blog.adacore.com/pointer-based-data-structures-in-sp...
9. 9.▲
   by yannickmoy 8y ago

   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.adacore.com/tetris-in-spark-on-ar
10. 10.▲
    by yannickmoy 9y ago

    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
11. 11.▲
    by yannickmoy 9y ago

    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 concept we're pus
12. 12.▲
    by yannickmoy 9y ago

    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 say "We wor
13. 13.▲
    by yannickmoy 9y ago

    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, this is well examplifie