LLVM project: SMACK Software Verifier


I would appreciate if you would add this project description to your
LLVM projects webpage:
SMACK Software Verifier

By <a href="GitHub - smackers/smack: SMACK Software Verifier and Verification Toolchain;

<a href="https://github.com/smackers/smack&quot;&gt;SMACK&lt;/a&gt; is an automated
software verifier, verifying assertions given in its input LLVM
intermediate representation (IR) programs. Under the hood, SMACK is a
translator from the LLVM IR into the Boogie intermediate verification
language (IVL). Targeting Boogie exploits a canonical platform which
simplifies the implementation of algorithms for verification, model
checking, and abstract interpretation.

Thanks in advance!

-- Zvonimir

Dear Zvonimir,

I've made the changes to the LLVM Projects page. In addition, I've added SMACK to the LLVM User's page (The LLVM Compiler Infrastructure Project). Please take a look at both and let me know if you're happy with the changes.

If you have any publications on SMACK that we haven't added to the LLVM Publications page, please let me know, and I'll add them.

Finally, it looks like you're using DSA as part of SMACK. Are you making updates to DSA or just using it as is? Are you using it for call graph analysis or also for its points-to analysis?

I'd like to gauge interest in points-to analysis and related analyses because I'd like to submit a BoF on the topic at this year's LLVM Developer's meeting. Points-to analysis is one of those things that has never really made it into LLVM mainline, but researchers keep needing it.


John Criswell