3 ms·

I haven't yet. This was my path to Frama-C: 1. Try writing C code that's "obviously safe." Gave up on that pretty quickly. 2. Maybe if I make all buffers glob

I haven't yet. This was my path to Frama-C: 1. Try writing C code that's "obviously safe." Gave up on that pretty quickly. 2. Maybe if I make all buffers global, I can verify some basics with a script. Gave up when I learned that "abstract interpretation" already exists, and it's way more advanced than anything I could whip up. (But kept the global buffers for now...) 3. The only example I found for a while was https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos, but it needed an old version of Clang, and my laptop didn't have enough memory to build it. 4. Found a couple other examples that were clearly someone's research project. 5. Finally found Frama-C by searching through Fedora packages. And it's exactly what I needed. There's definitely a learning curve, and it's not always obvious how to get it to do what you want. But I can at least install it, there's a nice GUI, and it's thoroughly documented. I didn't hear of CBMC until later, but I see there a Fedora package for that too. Should probably take a crack at it!

fdupress 4y ago
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.

fdupress 4y ago

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.