Hacker News new | ask | show | jobs
by throwaw12 2 days ago
these are impressive findings, I am curious what was your process to convert existing code to formal verification languages like TLA+.

My basic understanding was to verify high level abstractions (e.g. transport ACK, fsyncs and so on), but verifying this deep probably requires complete verification of stdlib methods used by Postgres, otherwise how can you pinpoint culprit is the sscanf?
1 comments
malisper 2 days ago
Right now I'm only doing very small simple functions. Kani[0] takes care of translating the code to an intermediate representation for me. It converts the Rust code and C code into a GOTO program[1] which verifiers can then run on top of

[0] https://github.com/model-checking/kani

[1] https://model-checking.github.io/cbmc-training/cbmc/overview...

link
touisteur 1 day ago
GOTO is back ! So glad to see CBMC used. I used to write translators to GOTO for simple code checking and was wondering where the recent state of the art was. Thanks for the pointers.

Did you have a look at why3 and generating verification conditions from Rust or C code (as frama-c does) ?

link