3 ms·

Research tools are getting closer to what people consider "real" programs, even if they often focus on embedded systems software. CompCert already deals with a

by dhekir 12y ago

Research tools are getting closer to what people consider "real" programs, even if they often focus on embedded systems software. CompCert already deals with a quite large subset of C. Frama-C can deal with most if not all syntactic features of C, but then the next challenge is the C standard library, e.g. specifying every useful function (and even "simple" ones such as memcpy can be quite tricky). Afterwards, you have to deal with the glibc, then other high-level libraries, etc... Most of these tools are either still in a mostly-academic setting (where "documentation = conference paper"), or do not have enough funding to pay for the development of more user-friendly features and extensive documentation. But with the ever-increasing security issues receiving media attention lately, we can hope more funding will allow these tools to reach a more mainstream status. By the way, could you give an example of a small program that you would consider "real"? Just to have an idea of its size and complexity.

rwmj 12y ago
Firstly I don't expect to prove a whole program. However being able to prove the correctness of key functions or algorithms in a program could be useful. You mention glibc, and it would be great to prove that (for example) 'qsort' is correct. That wouldn't be entirely trivial: https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/msort.c;h=4e17a8874736d7a653b3f589fbb7ad253225c939;hb=HEAD https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/msor... https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/qsort.c;h=304fbed8e5d8d2edfd606ab7db6412e408c1d479;hb=HEAD https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/qsor... For an example of a larger program, I'd like to prove various invariants of C programs, such as that 'reply_with_error' is called exactly once on every error path in this program: https://github.com/libguestfs/libguestfs/tree/master/daemon https://github.com/libguestfs/libguestfs/tree/master/daemon

by dhekir 12y ago

rwmj 12y ago

Firstly I don't expect to prove a whole program. However being able to prove the correctness of key functions or algorithms in a program could be useful. You mention glibc, and it would be great to prove that (for example) 'qsort' is correct. That wouldn't be entirely trivial: https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/msort.c;h=4e17a8874736d7a653b3f589fbb7ad253225c939;hb=HEAD https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/msor... https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/qsort.c;h=304fbed8e5d8d2edfd606ab7db6412e408c1d479;hb=HEAD https://sourceware.org/git/?p=glibc.git;a=blob;f=stdlib/qsor... For an example of a larger program, I'd like to prove various invariants of C programs, such as that 'reply_with_error' is called exactly once on every error path in this program: https://github.com/libguestfs/libguestfs/tree/master/daemon https://github.com/libguestfs/libguestfs/tree/master/daemon