KRust: A Formal Executable Semantics of Rust

From AcaWiki
Jump to: navigation, search

Citation: Feng Wang, Fu Song, Min Zhang, Xiaoran Zhu, Jun Zhang (2018/04/28) KRust: A Formal Executable Semantics of Rust.
Internet Archive Scholar (search for fulltext): KRust: A Formal Executable Semantics of Rust
Download: https://arxiv.org/abs/1804.10806
Tagged:

Summary

Describe Rust, for which formal semantics has not yet been well studied, which impedes further developments of formal analysis and verification tools for Rust programs.

Propose formal executable semantics KRust for Rust using the K framework, capturing:

  1. all Rust primitive types and their operations
  2. compound data types: struct, array and vector
  3. all basic control flow constructs: for, while, loop, if, if/else, function definition/call
  4. three most distinct and important features: ownership, borrow and lifetime

Test KRust against 157 tests from Rust test suite (of 3119) that KRust syntax supports, plus 25 hand-crafted tests to increase coverage.

Theoretical and Practical Relevance

This work is the first cornerstone of a "long-term program is to develop an almost complete formal executable semantics for Rust and formally verify Rust programs using formal analysis tools turned from the semantics".

Retrieved from "https://acawiki.org/index.php?title=KRust:_A_Formal_Executable_Semantics_of_Rust&oldid=11351"