SMACK swMATH ID: 23311 Software Authors: Carter, M., He, S., Whitaker, J., Rakamarić, Z., Emmi, M. Description: 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. Homepage: http://smackers.github.io/ Related Software: CBMC; z3; KLEE; CPAchecker; SeaHorn; VCC; Frama-C; UFO; LLVM; Crust; Viper; Joogie; Boogie; SMT-LIB; Cascade; SatAbs; BoogiePL; Predator; LLBMC; BVD Cited in: 8 Publications Standard Articles 1 Publication describing the Software Year SMACK: Decoupling source language details from verifier implementations Rakamarić, Zvonimir; Emmi, Michael 2014 all top 5 Cited by 25 Authors 1 Baranowski, Marek 1 Barrett, Clark W. 1 Beyer, Dirk 1 Bohlender, Dimitri 1 Cook, Byron 1 Dangl, Matthias 1 Garzella, Jack J. 1 Groves, Lindsay J. 1 He, Shaobo 1 Heljanko, Keijo 1 Khazem, Kareem 1 Kiefer, Moritz 1 Klebanov, Vladimir 1 Kowalewski, Stefan 1 Kröning, Daniel 1 Pearce, David J. 1 Rakamarić, Zvonimir 1 Saarikivi, Olli 1 Tasiran, Serdar 1 Tautschnig, Michael 1 Tuttle, Mark R. 1 Ulbrich, Mattias 1 Utting, Mark 1 Wendler, Philipp 1 Wies, Thomas Cited in 4 Serials 3 Journal of Automated Reasoning 1 Discrete Event Dynamic Systems 1 Formal Methods in System Design 1 Journal of Logical and Algebraic Methods in Programming Cited in 2 Fields 8 Computer science (68-XX) 1 Systems theory; control (93-XX) Citations by Year