SMACK is both a modular software verification toolchain and a self-contained software verifier. It can be used to verify the assertions in its input programs. In its default mode, assertions are verified up to a given bound on loop iterations and recursion depth; it contains experimental support for unbounded verification as well. Under the hood, SMACK is a translator from the LLVM compiler’s popular intermediate representation (IR) into the Boogie intermediate verification language (IVL). Sourcing LLVM IR exploits an increasing number of compiler front-ends, optimizations, and analyses. Targeting Boogie exploits a canonical platform which simplifies the implementation of algorithms for verification, model checking, and abstract interpretation.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Bohlender, Dimitri; Kowalewski, Stefan: Leveraging Horn clause solving for compositional verification of PLC software (2020)
- Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
- Chungha Sung, Brandon Paulsen, Chao Wang: CANAL: A Cache Timing Analysis Framework via LLVM Transformation (2018) arXiv
- Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
- Wang, Wei; Barrett, Clark; Wies, Thomas: Partitioned memory models for program analysis (2017)
- Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
- Rakamarić, Zvonimir; Emmi, Michael: SMACK: Decoupling source language details from verifier implementations (2014) ioport