KRust: A Formal Executable Semantics of Rust

doi:10.1109/TASE.2018.00014

	KRust: A Formal Executable Semantics of Rust
	Wang, Feng1 ; Song, Fu1 ; Zhang, Min 2; Zhu, Xiaoran 2; Zhang, Jun1
	2018
会议录名称	PROCEEDINGS 2018 12TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE 2018)
卷号	2018-January
页码	44-51
发表状态	已发表
DOI	10.1109/TASE.2018.00014
摘要	Rust 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.
关键词	Formal operational semantics Rust programming language K framework
出版地	345 E 47TH ST, NEW YORK, NY 10017 USA
会议地点	Guangzhou, China
会议日期	29-31 Aug. 2018
URL	查看原文
收录类别	CPCI ; CPCI-S ; EI
语种	英语
资助项目	NSFC[61502171]
WOS研究方向	Computer Science
WOS类目	Computer Science, Software Engineering
WOS记录号	WOS:000454985900006
出版者	IEEE
EI入藏号	20191006591251
EI主题词	High level languages ; Program interpreters ; Refuse collection ; Safety engineering ; Semantics
EI分类号	Municipal and Industrial Wastes; Waste Treatment and Disposal:452 ; Computer Software, Data Handling and Applications:723 ; Safety Engineering:914
原始文献类型	Proceedings Paper
来源库	IEEE
引用统计
文献类型	会议论文
条目标识符	https://kms.shanghaitech.edu.cn/handle/2MSLDSTB/29111
专题	信息科学与技术学院_硕士生信息科学与技术学院_PI研究组_宋富组
通讯作者	Wang, Feng
作者单位	1.ShanghaiTech Univ, Sch Informat Sci & Technol, Shanghai, Peoples R China 2.East China Normal Univ, Shanghai Key Lab Trustworthy Comp, Shanghai, Peoples R China
第一作者单位	信息科学与技术学院
通讯作者单位	信息科学与技术学院
第一作者的第一单位	信息科学与技术学院
推荐引用方式 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.