Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2018: Automated Technology for Verification and Analysis pp 528–535Cite as

Verifying Rust Programs with SMACK

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11138))

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.

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

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    For our tool and benchmarks see https://github.com/smackers/smack.

  2. 2.

    https://github.com/uutils/coreutils/issues/1195.

  3. 3.

    https://github.com/uutils/coreutils/issues/1194.

References

  1. Balasubramanian, A., Baranowski, M.S., Burtsev, A., Panda, A., Rakamarić, Z., Ryzhyk, L., et al.: System programming in rust: beyond safety. In: HotOS (2017)

    Google Scholar 

  2. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: FMCO (2005)

    Google Scholar 

  3. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: SMT (2010)

    Google Scholar 

  4. Cross-platform Rust rewrite of the GNU coreutils. https://github.com/uutils/coreutils

  5. de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS (2008)

    Google Scholar 

  6. Hahn, F.: Rust2Viper: building a static verifier for rust. Master’s thesis, ETH (2016)

    Google Scholar 

  7. He, S., Rakamarić, Z.: Counterexample-guided bit-precision selection. In: APLAS (2017)

    Google Scholar 

  8. Jung, R., Jourdan, J.-H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. In: POPL (2017)

    Google Scholar 

  9. Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: CAV (2012)

    Google Scholar 

  10. Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO (2004)

    Google Scholar 

  11. Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: CAV (2014)

    Google Scholar 

  12. The Rust programming language. https://www.rust-lang.org

  13. SMACK software verifier and verification toolchain. http://smackers.github.io

  14. Toman, J., Pernsteiner, S., Torlak, E.: CRUST: a bounded verifier for rust. In: ASE (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing, University of Utah, Salt Lake City, USA

    Marek Baranowski, Shaobo He & Zvonimir Rakamarić

Authors
  1. Marek Baranowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shaobo He
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zvonimir Rakamarić
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marek Baranowski .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, WA, USA

    Shuvendu K. Lahiri

  2. University of Southern California, Los Angeles, CA, USA

    Chao Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Baranowski, M., He, S., Rakamarić, Z. (2018). Verifying Rust Programs with SMACK. In: Lahiri, S., Wang, C. (eds) Automated Technology for Verification and Analysis. ATVA 2018. Lecture Notes in Computer Science(), vol 11138. Springer, Cham. https://doi.org/10.1007/978-3-030-01090-4_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01090-4_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-01089-8

  • Online ISBN: 978-3-030-01090-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation