SMACK

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.

• CANAL: A Cache Timing Analysis Framework via LLVM Transformation, Chungha Sung, Brandon Paulsen, Chao Wang, 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018)
• Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware, Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik, 55th Annual Design Automation Conference (DAC 2018)
• Reducer-Based Construction of Conditional Verifiers, Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, Heike Wehrheim, 40th International Conference on Software Engineering (ICSE 2018)
• ZEUS: Analyzing Safety of Smart Contracts, Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma, 25th Annual Network and Distributed System Security Symposium (NDSS 2018)
• Formal Verification of Optimizing Compilers, Yiji Zhang, Lenore D. Zuck, Keynote at the 14th International Conference on Distributed Computing and Internet Technology (ICDCIT 2018)
• Counterexample-Guided Bit-Precision Selection, Shaobo He, Zvonimir Rakamaric, 15th Asian Symposium on Programming Languages and Systems (APLAS 2017)
• FaCT: A Flexible, Constant-Time Programming Language, Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan, IEEE Secure Development Conference (SecDev 2017)
• Static Assertion Checking of Production Software with Angelic Verification, Shaobo He, Shuvendu Lahiri, Akash Lal, Zvonimir Rakamaric, 8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017)
• Refining Interprocedural Change-Impact Analysis using Equivalence Relations, Alex Gyori, Shuvendu Lahiri, Nimrod Partush, 26th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2017)
• System Programming in Rust: Beyond Safety, Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamaric, Leonid Ryzhyk, 16th Workshop on Hot Topics in Operating Systems (HotOS 2017)
• Verifying Constant-Time Implementations, Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi, 25th USENIX Security Symposium (2016)
• Statistical Similarity of Binaries, Yaniv David, Nimrod Partush, Eran Yahav, 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016)
• SMACK Software Verification Toolchain, Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi, Demonstrations Track at the 38th IEEE/ACM International Conference on Software Engineering (ICSE 2016)
• Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers, Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric, 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015)
• SMACK+Corral: A Modular Verifier (Competition Contribution), Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)
• ICE: A Robust Framework for Learning Invariants, Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider, 26th International Conference on Computer Aided Verification (CAV 2014)
• SMACK: Decoupling Source Language Details from Verifier Implementations, Zvonimir Rakamaric, Michael Emmi, 26th International Conference on Computer Aided Verification (CAV 2014) [MAIN REFERENCE]
• Modular Verification of Shared-Memory Concurrent System Software, Zvonimir Rakamaric, Ph.D. Thesis, Department of Computer Science, University of British Columbia, 2011
• A Scalable Memory Model for Low-Level Code, Zvonimir Rakamaric, Alan J. Hu, 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009)
• Automatic Inference of Frame Axioms Using Static Analysis, Zvonimir Rakamaric, Alan J. Hu, 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008)