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