Verification of Rust programs

#1

Hi everyone !

I recently started my PhD, the main topic of which is the verification of Rust programs. To clarify what it is, what it isn’t and how my work will interact with other efforts in that area, I’ve written a blog post that explains it all to Rust programmers.

During a case study, I fixed a Servo bug using formal methods, I hope this method of bug-fixing will be more frequent in the future :slight_smile:

25 Likes

#2

I am not a formal methods guy, but your blog post is so well written that I look forward to reading your thesis.

6 Likes

#3

Hi,

I love this and have been waiting/hoping for deductive verification in Rust for a while!

A few questions more or less specific to your subject:

Does F* support proving properties about concurrent/parallel programs?
If not would this require temporal logics like CTL*?
Do any of the existing verification techniques you mention in your blog post support parallelism or concurrency?

Why does F* have/need header files?

How compatible is F* with Rust code? I’ve heard of KreMLin which translates Low*, a subset of F* to verified C code, however it has several limitations, such as (correct me if I’m wrong) non-recursive datastructures.

Thanks for your time and efforts!

Best,
ambiso

2 Likes

#4

Unfortunately I think something happened to your blog. The post link consistently fails for me with ERR_CONNECTION_REFUSED (and I’m not having trouble with any other sites atm).

0 Likes

#5

Yeah, clearly it’s down i confirm… Some verified software failure here :wink:

0 Likes