Zvonimir Rakamaric
2014-Jun-02 19:31 UTC
[LLVMdev] Publication: "SMACK: Decoupling Source Language Details from Verifier Implementations"
Hi, So, SMACK is a software verifier based around LLVM, and you can find more info (PDF, title, abstract) about our recent publication here: http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/ I would appreciate if you could add it to your list of LLVM-based publications. Thanks! Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/
Criswell, John T
2014-Jun-02 19:57 UTC
[LLVMdev] Publication: "SMACK: Decoupling Source Language Details from Verifier Implementations"
I will add it, but I am away from the office most of this week and was not allowed to bring a laptop with me :). Please ping me if it's not done by close of business Friday this week. John Criswell Sent from my iPhone> On Jun 2, 2014, at 2:36 PM, "Zvonimir Rakamaric" <zvonimir at cs.utah.edu> wrote: > > Hi, > > So, SMACK is a software verifier based around LLVM, and you can find > more info (PDF, title, abstract) about our recent publication here: > http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/ > > I would appreciate if you could add it to your list of LLVM-based publications. > > Thanks! > > 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
2014-Jun-06 15:25 UTC
[LLVMdev] Publication: "SMACK: Decoupling Source Language Details from Verifier Implementations"
Dear Zvonimir, This is done. However, if you know how to get the accent over the last letter in your name, please let me know. I don't know how to convince HTML to do that. BTW, it's nice to see an LLVM to Boogie translator, and thanks for open-sourcing it. I suspect SMACK will be a useful tool. Regards, John Criswell On 6/2/14, 2:31 PM, Zvonimir Rakamaric wrote:> Hi, > > So, SMACK is a software verifier based around LLVM, and you can find > more info (PDF, title, abstract) about our recent publication here: > http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/ > > I would appreciate if you could add it to your list of LLVM-based publications. > > Thanks! > > 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
Zvonimir Rakamaric
2014-Jun-06 16:35 UTC
[LLVMdev] Publication: "SMACK: Decoupling Source Language Details from Verifier Implementations"
Thanks for taking care of this John and don't worry about my last name. I use 'c' all the time :). Yup, SMACK is gaining some traction, which is great... Best, -- Zvonimir -- http://zvonimir.info http://soarlab.org/ On Fri, Jun 6, 2014 at 9:25 AM, John Criswell <criswell at illinois.edu> wrote:> Dear Zvonimir, > > This is done. However, if you know how to get the accent over the last > letter in your name, please let me know. I don't know how to convince HTML > to do that. > > BTW, it's nice to see an LLVM to Boogie translator, and thanks for > open-sourcing it. I suspect SMACK will be a useful tool. > > Regards, > > John Criswell > > > On 6/2/14, 2:31 PM, Zvonimir Rakamaric wrote: >> >> Hi, >> >> So, SMACK is a software verifier based around LLVM, and you can find >> more info (PDF, title, abstract) about our recent publication here: >> >> http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/ >> >> I would appreciate if you could add it to your list of LLVM-based >> publications. >> >> Thanks! >> >> 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 > >
Possibly Parallel Threads
- Publication: "Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers"
- [LLVMdev] LLVM is doing something a bit weird in this example (which messes up DSA)
- [LLVMdev] Adding SMACK to the list of LLVM projects
- [LLVMdev] Adding SMACK to the list of LLVM projects
- [LLVMdev] Adding SMACK to the list of LLVM projects