摘要:
This thesis presents, to our knowledge, the first attempt at utilizing Pointer Assertion Logic and monadic second-order logic in the context of pointer ma- nipulation in Rust, as well as the application of Graph types for specifying Data Structure Invariants (DI) and demonstrating preservation of Rust data structures. We formulated a transformation from MIR to P ALE and demonstrated its application on a concrete example of a data structure manipulation program in Rust. We then attempted to prove the memory safety of this example and showed that the program does not violate the DI. We have identified that P ALE and monadic second-order logic present interesting avenues for further research in formal verification. We believe that these approaches have the potential to advance the field of formal verification in the context of Rust.