Viewing profile — 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)…

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

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 …

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

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

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

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

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 …

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…

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

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

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

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

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

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

In fact that would be ``` 0 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 comp…

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. The…