Abstract

Rust is an emerging systems programming language with guaranteed memory safety and modern language features that has been extensively adopted to build safety-critical software. However, there is currently a lack of automated software verifiers for Rust. In this work, we present our experience extending the SMACK verifier to enable its usage on Rust programs. We evaluate SMACK on a set of Rust programs to demonstrate a wide spectrum of language features it supports.

Citation

Marek Baranowski, Shaobo He, Zvonimir Rakamaric
Verifying Rust Programs with SMACK
Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA), 11138: 528--535, doi:10.1007/978-3-030-01090-4_32, 2018.

BibTeX

@inproceedings{2018_atva_bhr,
  title = {Verifying Rust Programs with SMACK},
  author = {Marek Baranowski and Shaobo He and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA)},
  series = {Lecture Notes in Computer Science},
  volume = {11138},
  publisher = {Springer},
  editor = {Shuvendu K. Lahiri and Chao Wang},
  pages = {528--535},
  doi = {10.1007/978-3-030-01090-4_32},
  year = {2018}
}

Acknowledgements

Supported in part by the National Science Foundation (NSF) award CNS 1527526.

Abstract

Citation

BibTeX

Acknowledgements

Resources