Frama-C

Joe Nelson joe at begriffs.com
Sun Jun 30 03:28:27 UTC 2019


Hi Sam, thanks for giving your presentation, I enjoyed it. Forgot how
many UB items were listed in Annex J so it was a fun exercise when you
asked the audience to estimate it.

I found the frama-c prover particularly interesting. Looks like there's
an OpenBSD port [0] so I could install it on our shared server. Would
you be interested in pairing with me to prove the correctness of some
simple pure functions? For instance I wrote these functions [1] from
string.h as an exercise, and perhaps they can be proven correct.

0: http://ports.su/devel/frama-c
1: https://github.com/begriffs/libc/blob/master/string.c


More information about the Friends mailing list