KRust: A Formal Executable Semantics of Rust
Wang, Feng1; Song, Fu1; Zhang, Min2; Zhu, Xiaoran2; Zhang, Jun1
AbstractRust is a new and promising high-level system programming language. It provides both memory safety and thread safety through its novel mechanisms such as ownership, moves and borrows. Ownership system ensures that at any point there is only one owner of any given resource. The ownership of a resource can be moved or borrowed according to the lifetimes. The ownership system establishes a clear lifetime for each value and hence Rust does not necessarily need garbage collection. These novel features bring Rust high performance, fine-grained low-level control over memory without garbage collection, which differentiate Rust from other existing prevalent languages. For formal analysis of Rust programs and helping programmers learn its new mechanisms and features, a formal semantics of Rust is desired and useful as a fundament for developing related tools. In this paper, we present a formal executable operational semantics of a subset of Rust, called KRust. The semantics is defined in K, a rewriting-based executable semantic framework for programming languages. The executable semantics yields automatically a formal interpreter and verification tools for Rust programs. KRust has been validated by testing with 182 tests, including 157 tests from the official Rust test suite. We individually found an error in the Rust compiler.
KeywordFormal operational semantics Rust programming language K framework
Publication Place345 E 47TH ST, NEW YORK, NY 10017 USA
Conference PlaceGuangzhou, China
Indexed ByCPCI ; EI
Funding ProjectNSFC[61502171]
WOS Research AreaComputer Science
WOS SubjectComputer Science, Software Engineering
WOS IDWOS:000454985900006
EI Accession Number20191006591251
EI KeywordsHigh level languages ; Program interpreters ; Refuse collection ; Safety engineering ; Semantics
EI Classification NumberMunicipal and Industrial Wastes; Waste Treatment and Disposal:452 ; Computer Software, Data Handling and Applications:723 ; Safety Engineering:914
Original Document TypeProceedings Paper
Citation statistics
Cited Times:2[WOS]   [WOS Record]     [Related Records in WOS]
Document Type会议论文
Corresponding AuthorWang, Feng
Affiliation1.ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai, Peoples R China
2.East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China
First Author AffilicationSchool of Information Science and Technology
Corresponding Author AffilicationSchool of Information Science and Technology
First Signature AffilicationSchool of Information Science and Technology
Recommended Citation
GB/T 7714
Wang, Feng,Song, Fu,Zhang, Min,et al. KRust: A Formal Executable Semantics of Rust[C]. 345 E 47TH ST, NEW YORK, NY 10017 USA:IEEE,2018:44-51.
Files in This Item: Download All
File Name/Size DocType Version Access License
TASE18.pdf(194KB)会议论文 开放获取CC BY-NC-SAView Download
Related Services
Usage statistics
Scholar Google
Similar articles in Scholar Google
[Wang, Feng]'s Articles
[Song, Fu]'s Articles
[Zhang, Min]'s Articles
Baidu academic
Similar articles in Baidu academic
[Wang, Feng]'s Articles
[Song, Fu]'s Articles
[Zhang, Min]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Wang, Feng]'s Articles
[Song, Fu]'s Articles
[Zhang, Min]'s Articles
Terms of Use
No data!
Social Bookmark/Share
File name: TASE18.pdf
Format: Adobe PDF
All comments (0)
No comment.

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.