Verifying Rust Programs with SMACK

Share

Marek Baranowski, Shaobo He, Zvonimir Rakamaric. 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Los Angeles, CA, USA.
[pdf] [bib]

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.

Bibtex:

@inproceedings{atva2018-bhr,
  author = {Marek Baranowski and Shaobo He and Zvonimir Rakamari\'c},
  title = {Verifying {Rust} Programs with {SMACK}},
  booktitle = {Proceedings of the 16th International Symposium on
    Automated Technology for Verification and Analysis (ATVA)},
  year = {2018},
  note = {to appear},
}