A Comparative Study on Deductive Verification for Rust and C
Abstract: In programming, deductive verification is a technique to generate proof that a function obeys a set of manually specified regulations in the form of annotations. In addition to these annotations, the verifier also utilizes the constraints of the underlying programming language to prove that the function cannot cause the program to crash unexpectedly. This thesis investigates how the type system of Rust, specifically built-in memory-safety guarantees, can affect the amount and types of annotations required for a verifier to generate a proof of the correctness of a function, as compared to C. This was done by comparing the differences in the annotations required to verify example functions in Rust and C, using their respective verification tools, Prusti and Frama-C. The results show that the number of required annotations for a function implemented in C is higher when compared to Rust. Furthermore, the annotations used in Rust were a strict subset of those in C for the functions tested. This indicates that the memory-safety guarantees present in Rust play a role in the practicality of annotating functions for deductive verification. However, future work with more data and verification tools with a richer feature set is needed to draw more precise conclusions.
AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)