3 ms·

Ada, even with Spark, has formal verification capabilities that are nowhere near what has been achieved for C with Frama-C. With Frama-C you can prove that arbi

Ada, even with Spark, has formal verification capabilities that are nowhere near what has been achieved for C with Frama-C. With Frama-C you can prove that arbitrary heap allocated data structures with pointers are bug-free. You can’t do this with Ada Spark.

jes 5y ago
Link to a slide deck on Frama-C: https://cse.msu.edu/~cse814/Lectures/frama-c.pdf https://cse.msu.edu/~cse814/Lectures/frama-c.pdf
nine_k 5y ago
How much does Frama-C limit the ways you can write C code? How long does it take to check a reasonably sized code base?
AlexCoventry 5y ago
> you can prove that arbitrary heap allocated data structures with pointers are bug-free Can you say a bit more about that? The way that's written, it sounds like a solution to the halting problem.
- curtisf 5y ago
  _Finding_ a proof is undecidable. _Verifying_ that a proof is correct is easy (it's usually linear-ish in the length of the proof). If the programmer supplies (most of) the proof, a compiler can easily certify that the proof is correct with respect to its model of the program. Still, constraint solvers (often SMT solvers) can succeed a lot of the time (just not _all_ of the time) in automating pieces of proofs, so all the tedium doesn't need to be left with the programmer. In particular, generally programmers write code that they believe is correct, so if they're right then there's usually a straightforward proof that it is correct since their beliefs will only get so complicated.
  - AlexCoventry 5y ago
    Ah, arbitrary heap-allocated structures a human can supply a proof for. Thanks; makes sense.
  - sterlind 5y ago
    my only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly vague on what remaining obligations need to be discharged. You have to stumble around in the dark, trying asserts and assumes, until you narrow down where it got stumped. are there other automated-proof languages that do a better job on this?

jes 5y ago

Link to a slide deck on Frama-C: https://cse.msu.edu/~cse814/Lectures/frama-c.pdf https://cse.msu.edu/~cse814/Lectures/frama-c.pdf

nine_k 5y ago

How much does Frama-C limit the ways you can write C code? How long does it take to check a reasonably sized code base?

AlexCoventry 5y ago

> you can prove that arbitrary heap allocated data structures with pointers are bug-free Can you say a bit more about that? The way that's written, it sounds like a solution to the halting problem.

curtisf 5y ago
_Finding_ a proof is undecidable. _Verifying_ that a proof is correct is easy (it's usually linear-ish in the length of the proof). If the programmer supplies (most of) the proof, a compiler can easily certify that the proof is correct with respect to its model of the program. Still, constraint solvers (often SMT solvers) can succeed a lot of the time (just not _all_ of the time) in automating pieces of proofs, so all the tedium doesn't need to be left with the programmer. In particular, generally programmers write code that they believe is correct, so if they're right then there's usually a straightforward proof that it is correct since their beliefs will only get so complicated.
- AlexCoventry 5y ago
  Ah, arbitrary heap-allocated structures a human can supply a proof for. Thanks; makes sense.
- sterlind 5y ago
  my only experience in this area is Dafny, which aggressively automates the proof-finding (by passing it to Z3), but when that fails the compiler is exceedingly vague on what remaining obligations need to be discharged. You have to stumble around in the dark, trying asserts and assumes, until you narrow down where it got stumped. are there other automated-proof languages that do a better job on this?