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