Hacker News Reader

Comment by kobebrookskC3 | Hacker News Reader

these are relatively small, relatively self-contained algorithms and data structures though, right? not a "big" piece of software.

View on HN

"Big" software is mostly not difficult algorithms, but writing boilerplate glue code that connects the inputs and outputs of algorithms/functions that are usually written by someone else. Frama-C can definitely verify the boilerplate for "big" software, this is actually easier than verifying data structures and algorithms, which requires knowing the key property to get the prover to see that the algorithm always makes progress toward a solution. Once you have the contracts set up for calling a function, Frama-C will enforce that the contract is always met.

The CompCert verified C compiler is "big" software, but not actually written in C, rather OCaml and Coq/Gallina.

supposing a compiler, was written in c, would frama-c be able to get similar guarantees that coq allows for compcert?

also, what happens when the loop invariants can't be automatically proved? is there some way to manually prove invariants hold?

Yes, a compiler written in C could be verified with Frama-C, but "verifying in Frama-C" for something that hard (i.e. has many proof steps that cannot be automated) really means verifying in a proof assistant that can interact with Frama-C that understands ACSL, and Coq is usually used. And indeed, the loop invariants you mention usually cannot be automatically proved and must be proved manually, which is why there is such a learning curve to Frama-C. I first started using Frama-C without having used Coq/Gallina/OCaml, and I began to learn them simply because I hit a roadblock with Frama-C where I couldn't really progress without a deeper understanding for why automatic proving fails when it fails, why the error messages when automatic proving fails often aren't terribly helpful, what the current limits of automatic proving are, how the automatic proving actually works under the hood, etc.

Coq has been used to formally verify a large body of classical mathematics. Coq can 'understand' what a prime number is and can be used to prove that there are infinitely many primes, can prove that sqrt(2) is irrational, etc. Coq can prove a recursive solver for the Towers of Hanoi actually solves the problem, etc. And thus Coq can prove a C program to solve the Towers of Hanoi correctly solves the problem, because Coq can reason about C programs.

I've been slowly working through the Software Foundations series on using Coq/Gallina:

https://softwarefoundations.cis.upenn.edu/

Another poster mentioned CBMC which I just started playing with. It is much less powerful than Frama-C, there isn't the ACSL specification capability and theorem proving, but it is much more automatic and much faster to get started with. For many cases if I just want to verify that a certain C file frees all its mallocs, doesn't have out-of-bounds accesses, and that all obviously bounded loops terminate, CBMC is much easier. Also, like Frama-C, it converts C functions into "goto programs" (removes the syntactic sugar of 'for' and 'while' loops to obtain a more pure Control-Flow-Graph (CFG)) for certain forms of analysis, and when I first encountered this in Frama-C there was no explanation why, whereas the manual for CBMC actually has an excellent gentle introduction:

http://cprover.diffblue.com/background-concepts.html

Reply on news.ycombinator.com