Dear Zvonimir,
I've made the changes to the LLVM Projects page. In addition, I've
added SMACK to the LLVM User's page (http://llvm.org/Users.html).
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.
Regards,
John Criswell
On 4/21/15 12:34 PM, Zvonimir Rakamaric wrote:> Hi,
>
> I would appreciate if you would add this project description to your
> LLVM projects webpage:
> SMACK Software Verifier
>
> By <a
href="https://github.com/smackers/smack/wiki/Smackers">smackers</a>
>
> <a href="https://github.com/smackers/smack">SMACK</a>
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!
>
> Best,
> -- Zvonimir
>
> --
> http://zvonimir.info
> http://soarlab.org/
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
--
John Criswell
Assistant Professor
Department of Computer Science, University of Rochester
http://www.cs.rochester.edu/u/criswell