11 ms·

You're waiting for a tutorial on Coq integrated with Frama-C, or for a tutorial on any of them?

by dhekir 12y ago

rwmj 12y ago
I'm waiting for a tutorial on how to prove correctness of either OCaml or (especially) C code in real programs.
- vstolz 12y ago
  It is possible, see e.g. http://ssrg.nicta.com.au/projects/TS/ http://ssrg.nicta.com.au/projects/TS/, though it's not really the tutorial you've been hoping for.
- 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

You're waiting for a tutorial on Coq integrated with Frama-C, or for a tutorial on any of them?

by dhekir 12y ago

You're waiting for a tutorial on Coq integrated with Frama-C, or for a tutorial on any of them?

rwmj 12y ago

I'm waiting for a tutorial on how to prove correctness of either OCaml or (especially) C code in real programs.

vstolz 12y ago
It is possible, see e.g. http://ssrg.nicta.com.au/projects/TS/ http://ssrg.nicta.com.au/projects/TS/, though it's not really the tutorial you've been hoping for.
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