KsassPeuk

Well, Frama-C is maintained thanks to public funding (Europe/France) and industrial users who use it for actual certification of systems. For example, Thales (Common Criteria EAL7), Airbus (DO-178C), EDF (ISO 60880). I don't know what you mean by professional tool if this is not professional ;)

At some point in the past you also posted the ACSL cast badly documented. I asked you what you needed exactly, but you probably missed the message. So let me try again:

What kind of documentation would you expect in addition to ACSL by Example and the WP tutorial?

In all its generality, the problem is undecidable. But there are quite a lot of tools that are meant to formally verify properties about programs. Proof assistants, of course, but there are also tools for more mainstream languages, like Frama-C, Ada/Spark, Java/KeY, Creusot (Rust), etc.

Well, Frama-C uses a quite modified version of CIL.

As a Frama-C developer, and more precisely the deductive verification tool, I'd say that formal proof of programs (especially proof that the program conforms to its specification) would be significantly easier on Rust. The main reason is related to the handling of memory aliases which is a nightmare in C, and that generates formulas that kill SMT solvers. The consequence is that the ongoing development tend to target something that has a lot in common with Rust: we try to assume memory separation most of the time, and check that it is true on function call, but it as harder to do it than with a type system.

What do you mean by "non determinism of solvers"? AFAIK, unless your proof finishes really close to the timeout, it is pretty uncommon that a failed PO suddenly succeeds and vice-versa if the code/the annotation are not modified.

> ACSL is badly documented/hard to learn, and you really want the proprietary stuff for anything nontrivial.

That's interesting. What kind of documentation would you expect in addition to ACSL by Example and the WP tutorial?

What are the proprietary components that you miss the most?

Frama-C is used in production to meet normative requirements for critical software at least at Airbus (DO-178C), THALES (CC EAL6/7), EDF (ISO 60880). I think that they use actual software in production.

On this kind of analysis, it strongly depends on the features that are used in the analyzed code and its degree of complexity. An analysis that is entirely automatic, detect every mistake and only mistakes is not possible in the general case.

For C, Frama-C + Eva plug-in does essentially the same job as Astrée (with small differences of support for specific features) and is open-source and freely available.

(There is an experimental C++ front-end, but it is not ready for industrial size C++ that makes extensive use of the standard library)

Speaking about tools like Frama-C, it is important to note that while there is an overhead during development of Rust programs because of the type system, proving the absence of runtime errors in industrial size programs using Frama-C is not something easy, and it remains quite costly (and to be fair, far more costly than making Rust programs type). However, it is true that you can catch some errors that are not caught by the Rust type system, say for example, integer overflows. But I would not bet that all problems caugth thanks to the type system of Rust can be caught using Frama-C.

Now, if we focus on functional properties (proving that the code is correct), one terribly hard problem when dealing with real world programs is handling the shape of the memory. That can make some proofs awful and really hard to complete. In a language like Rust, you can get a lot of information about the shape of the memory and the memory separation for free thanks to the type system. That would make proofs really easier (this is for example what is done, but with far less precision than what the Rust type system could provide, in the different memory models configuration in Frama-C/WP and it can already dramatically improve proof performance).

It probably does not justify rewrite everything, nor changing verification tools chains that are in use in some critical domains. However, I would definitely love working on and working with a Frama-Rust tool ;)

For the sake of completeness: Frama-C (+ WP plugin) can verify that the program conforms to the first specification, however, it indeed can't verify that the program does not contain an undefined behavior (reason why we write the second specification).

In fact there exists a plugin that can do that but it is currently not free:

https://frama-c.com/fc-plugins/mthread.html

(And by the way since it is not done by typing it is hard to use on legacy code)

> but much more limited

I agree and I disagree ;)

I agree because having a type system that directly provides the guarantee that whole classes of runtime error cannot happen provides fast feedback during development at a low cost.

I disagree because even in a press button (+ tuning) approach, you can prove things with Frama-C that the Rust compiler cannot prove (reason why there is runtime bound-checking, implementation defined behavior for integer overflow and so on in Rust). But also because you can prove much more advance properties than "just" absence of runtime errors.

You can have a look to this recent paper for example:

https://www.springerprofessional.de/en/formal-verification-o...

Another big example is the fact that Frama-C/WP is used for formal verification of some functional properties in aircraft software.

> Frama-C doesn't need to know anything about the target arch.

In fact, it needs some knowledge, but this knowledge can be configured for the project under analysis. This is the reason why the Frama-C kernel provides the `-machdep` option ;) .

Then depending on your code, you might need to add particular knowledge according to your target platform. For example validity of some hardware memory location, etc.

In fact that would be

``` 0 <= i <= n ```

As the loop reaches this value to terminate. Else, we could not deduce for example that `i = n` at the end of the loop (`0 <= i <= n && !(i < n)`).

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.

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.