[LLVMdev] LLVM project: SMACK Software Verifier

John Criswell jtcriswel at gmail.com
Thu Apr 23 08:00:23 PDT 2015


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




More information about the llvm-dev mailing list