4 ms·

Has anyone used the KeY project in industry? I'd certainly prefer proofs over unit tests. However, I don't understand formal proof systems sufficiently well to

by bglazer 12y ago

Has anyone used the KeY project in industry? I'd certainly prefer proofs over unit tests. However, I don't understand formal proof systems sufficiently well to know whether these they would work in terms of your typical "app" that makes RPC calls, DB changes, and generally has lots of moving parts and statefulness.

rwmj 12y ago
I have tried to use Coq and Frama-C to prove commercial OCaml and C programs, without, it has to be said, any success. I'm waiting for someone to write the brilliant tutorial.
- 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

by bglazer 12y ago

rwmj 12y ago

I have tried to use Coq and Frama-C to prove commercial OCaml and C programs, without, it has to be said, any success. I'm waiting for someone to write the brilliant tutorial.

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