[the_french]

I'm starting my PhD under the supervision of one of the Frama-C authors, if you have questions I can relay them.

In general I've found deductive verification techniques interesting / promising because they free engineers of a lot of required but tedious details you'd have in ITPs.

However, I think there's a LOT of room for improvement in terms of ergonomics of proof debugging. For a frequent (for me) problem when debugging invariants is conditionals that break the invariant.

if i have some code doing something like

    while (X) {
      invariant { forall i. 0 <= i < N .... }
      if j < i A else B 
    }

But it turns out that one of the branches A, B doesn't preserve the invariant well all the provers will tell me is 'can't prove this!' it's up to you to perform the transformations that split the two cases (granted in this example it's trivial) so that you can see that only _one_ branch was failing.

I think that there should be transforms that automatically do things like split the range of an interval along relevant points (aka j) to help you figure out which portions are failing.

There are tons of other issues related to proof ergonomics that could be improved, the UIs are really stuck in the 90s!

[aidenn0]

Is frama-c still limited to single-threaded debugging? I know in the general case a context-switch is the same as "call any function anywhere in your code at any point into it" but it would be nice if it had a way for me to teach it about my expected threading invarients (e.g. prove that these objects never escape the current thread of execution).

[KsassPeuk]

Note that most Frama-C analysis are not debugging tools. Although you can find bugs with them, they mostly focus on proving that there are no bugs, which is slightly different.

There are plugins for multi-thread programs.

One is an experimental plugin called Conc2Seq that I developed during my thesis with a focus on proving properties about small modules with a few functions accessing concurrently some global resources. Note however hat it is very experimental and it is not actively developed anymore, but at least it can be updated or give some ideas on how to write such an analyzer.

The second is a proprietary plugin called MThread (base on the Eva analysis of Frama-C), but it is only available via licensing.

[mcguire]

What's the status of handling manual memory management? The last time I looked, that was a huge, gaping hole in both Spark and Frama-C provers.

[KsassPeuk]

It depends on the verification tool you use.

Eva (the abstract interpreter) has different ways to model dynamic allocation. It is thus a tradeoff to find between precision and computation time.

WP does not have dynamic allocation support. This is an ongoing work, but it will not be available in the next release. Note that there are different ways to model the behavior of dynamic allocation, generally via axiomatic definitions and/or ghosts.