3 ms·

You could also try VeriFast [0], which is closer to Frama-C than CBMC. (VeriFast and Frama-C are deductive verification tools, CBMC is a bounded model checking

You could also try VeriFast [0], which is closer to Frama-C than CBMC. (VeriFast and Frama-C are deductive verification tools, CBMC is a bounded model checking tool.) It is slightly less approachable than Frama-C because it uses separation logic, but it's slightly more approachable because it uses symbolic execution, which allows it to display an actual execution trace that causes the failure. (You can then inspect that and decide whether your code or model is wrong.) [0]: https://github.com/verifast/verifast https://github.com/verifast/verifast

naasking 4y ago
Good reference, I had actually starred that on github to refer to later and totally forgot about it. Do you know of a review of the various open source verification tools available for C? The ones I'm aware of: CBMC, Frama-C, VeriFast, ESBMC. I've found papers like [1] which benchmark various model checkers, but no evaluation of the verification effort required for the various approaches. Edit: the tutorial for VeriFast does not make it look very usable compared to Frama-C's ACSL language. Their tutorial doesn't explain a bunch of the syntax or why they made certain choices, so it all feels very unergonomic. Edit 2: The SV-COMP competition on software verification [2] tests a whole bunch of tools, but Frama-C and VeriFast are not among them. Looks like CPAChecker [3] has the best power-to-weight ratio if you're looking for one tool to learn with the most errors caught across all benchmarks. [1] https://arxiv.org/abs/2003.11689 https://arxiv.org/abs/2003.11689 [2] https://sv-comp.sosy-lab.org/2020/ https://sv-comp.sosy-lab.org/2020/ [3] https://cpachecker.sosy-lab.org/ https://cpachecker.sosy-lab.org/
- fdupress 4y ago
  No, sorry; I'm not aware of proper comparisons for C verification tools, or at least recent and maintained tools. SV-COMP tends to propose a huge number of relatively simple tasks, which attracts model checkers and static analysers. Frama-C and VeriFast are functional verification tools. You can use them as static analysers, but there's a barrier to entry in terms of minimal required annotations that might not be present for tools designed for static analysis.

naasking 4y ago

Good reference, I had actually starred that on github to refer to later and totally forgot about it. Do you know of a review of the various open source verification tools available for C? The ones I'm aware of: CBMC, Frama-C, VeriFast, ESBMC. I've found papers like [1] which benchmark various model checkers, but no evaluation of the verification effort required for the various approaches. Edit: the tutorial for VeriFast does not make it look very usable compared to Frama-C's ACSL language. Their tutorial doesn't explain a bunch of the syntax or why they made certain choices, so it all feels very unergonomic. Edit 2: The SV-COMP competition on software verification [2] tests a whole bunch of tools, but Frama-C and VeriFast are not among them. Looks like CPAChecker [3] has the best power-to-weight ratio if you're looking for one tool to learn with the most errors caught across all benchmarks. [1] https://arxiv.org/abs/2003.11689 https://arxiv.org/abs/2003.11689 [2] https://sv-comp.sosy-lab.org/2020/ https://sv-comp.sosy-lab.org/2020/ [3] https://cpachecker.sosy-lab.org/ https://cpachecker.sosy-lab.org/

fdupress 4y ago
No, sorry; I'm not aware of proper comparisons for C verification tools, or at least recent and maintained tools. SV-COMP tends to propose a huge number of relatively simple tasks, which attracts model checkers and static analysers. Frama-C and VeriFast are functional verification tools. You can use them as static analysers, but there's a barrier to entry in terms of minimal required annotations that might not be present for tools designed for static analysis.