KsassPeuk

4 ms·

1.
by KsassPeuk 1y ago
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
2.
by KsassPeuk 2y ago
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 Exam
3.
by KsassPeuk 2y ago
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 Fra
4.
by KsassPeuk 2y ago
Well, Frama-C uses a quite modified version of CIL.
5.
by KsassPeuk 2y ago
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
6.
by KsassPeuk 2y ago
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 modif
7.
by KsassPeuk 3y ago
> 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? Wh
8.
by KsassPeuk 3y ago
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.
9.
by KsassPeuk 4y ago
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 cas
10.
by KsassPeuk 4y ago
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 industr
11.
by KsassPeuk 4y ago
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 no
12.
by KsassPeuk 4y ago
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 secon
13.
by KsassPeuk 4y ago
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)
14.
by KsassPeuk 4y ago
> 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 disa
15.
by KsassPeuk 5y ago
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 functio
16.
by KsassPeuk 5y ago
> 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`
17.
by KsassPeuk 6y ago
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)`).
18.
by KsassPeuk 6y ago
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. T
19.
by KsassPeuk 6y ago
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 experime