## Publications


### Main Reference

Please use the following publication when citing SMACK in your papers:  
[SMACK: Decoupling Source Language Details from Verifier Implementations](https://soarlab.org/publications/2014_cav_re),
Zvonimir Rakamaric, Michael Emmi,
26th International Conference on Computer Aided Verification (CAV 2014)


### Other Publications

This is an incomplete list of publications that use, leverage, or extend SMACK.
If you have a publication for this list, please email [Zvonimir](mailto:zvonimir@cs.utah.edu).

1. [CANAL: A Cache Timing Analysis Framework via LLVM Transformation](https://dl.acm.org/citation.cfm?id=3240485),
Chungha Sung, Brandon Paulsen, Chao Wang,
33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018)

1. [Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware](https://dl.acm.org/citation.cfm?id=3196055),
Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik,
55th Annual Design Automation Conference (DAC 2018)

1. [Reducer-Based Construction of Conditional Verifiers](https://dl.acm.org/citation.cfm?id=3180259),
Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, Heike Wehrheim,
40th International Conference on Software Engineering (ICSE 2018)

1. [ZEUS: Analyzing Safety of Smart Contracts](https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-1_Kalra_paper.pdf),
Sukrit Kalra, Seep Goel, Mohan Dhawan, Subodh Sharma,
25th Annual Network and Distributed System Security Symposium (NDSS 2018)

1. [Formal Verification of Optimizing Compilers](https://link.springer.com/chapter/10.1007/978-3-319-72344-0_3),
Yiji Zhang, Lenore D. Zuck,
Keynote at the 14th International Conference on Distributed Computing and Internet Technology (ICDCIT 2018)

1. [Counterexample-Guided Bit-Precision Selection](https://soarlab.org/publications/2017_aplas_hr),
Shaobo He, Zvonimir Rakamaric,
15th Asian Symposium on Programming Languages and Systems (APLAS 2017)

1. [FaCT: A Flexible, Constant-Time Programming Language](https://cseweb.ucsd.edu/~dstefan/pubs/cauligi:2017:fact.pdf),
Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan,
IEEE Secure Development Conference (SecDev 2017)

1. [Static Assertion Checking of Production Software with Angelic Verification](https://soarlab.org/publications/2017_tapas_hllr),
Shaobo He, Shuvendu Lahiri, Akash Lal, Zvonimir Rakamaric,
8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017)

1. [Refining Interprocedural Change-Impact Analysis using Equivalence Relations](https://www.microsoft.com/en-us/research/publication/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)

1. [System Programming in Rust: Beyond Safety](https://soarlab.org/publications/2017_hotos_bbbprr),
Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda,
Zvonimir Rakamaric, Leonid Ryzhyk,
16th Workshop on Hot Topics in Operating Systems (HotOS 2017)

1. [Verifying Constant-Time Implementations](https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida),
Jose Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Francois Dupressoir, Michael Emmi,
25th USENIX Security Symposium
(2016)

1. [Statistical Similarity of Binaries](http://dl.acm.org/citation.cfm?id=2908126),
Yaniv David, Nimrod Partush, Eran Yahav,
37th ACM SIGPLAN Conference on Programming Language Design and Implementation
(PLDI 2016)

1. [SMACK Software Verification Toolchain](https://soarlab.org/publications/2016_icse_chwre),
Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi,
Demonstrations Track at the 38th IEEE/ACM International Conference on Software Engineering (ICSE 2016)

1. [Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers](https://soarlab.org/publications/2015_ase_ddr),
Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric,
30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015)

1. [SMACK+Corral: A Modular Verifier (Competition Contribution)](https://soarlab.org/publications/2015_tacas_hcelqr),
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)

1. [ICE: A Robust Framework for Learning Invariants](http://madhu.cs.illinois.edu/CAV14ice.pdf),
Pranav Garg, Christof Löding, P. Madhusudan, Daniel Neider,
26th International Conference on Computer Aided Verification (CAV 2014)

1. [Modular Verification of Shared-Memory Concurrent System Software](https://soarlab.org/publications/2011_thesis_rakamaric),
Zvonimir Rakamaric,
Ph.D. Thesis, Department of Computer Science, University of British Columbia, 2011

1. [A Scalable Memory Model for Low-Level Code](https://soarlab.org/publications/2009_vmcai_rh),
Zvonimir Rakamaric, Alan J. Hu,
10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009)

1. [Automatic Inference of Frame Axioms Using Static Analysis](https://soarlab.org/publications/2008_ase_rh),
Zvonimir Rakamaric, Alan J. Hu,
23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008)