[LLVMdev] Publication Generation of TLM Testbenches Using Mutation Testing

[John Criswell]

On 1/30/13 11:42 AM, Marcelo Sousa wrote:
> Dear all,

I've put these two publications up on the LLVM publications page. One 
question I have is whether the URL on Alper Sen's page provides a free 
copy of the paper (I can't tell because my university has automatic 
access to all ACM publications).

Also, you mentioned that you formalized the LLVM IR.  You might be 
interested in the work of Jianzhou Zhao at the University of 
Pennsylvania.  They created a formal semantics for LLVM IR and used it 
to build verified transforms.  You can see the paper at 
http://www.cis.upenn.edu/~stevez/papers/ZNMZ12.pdf.

You might find the work of Grigore Rosu's group interesting.  They 
developed a formal semantics for C, and I want to say that they might 
have done the same for LLVM, although my memory's a bit fuzzy on that.  
In any event, the relevant publications are by Chucky Ellison at 
http://fsl.cs.illinois.edu/index.php/K_and_Matching_Logic.

-- John T.

>
> I would like to share a paper I co-authored with Prof. Alper Sen. This
> paper describes an algorithm to generate testbenches from SystemC
> models represented with LLVM IR. It was accepted and presented at
> International Conference on Hardware/Software Codesign and System
> Synthesis (CODES/ISSS), 2012. A link to the paper is accessible from
> acm or Alper's website:
> http://dl.acm.org/citation.cfm?id=2380498
> http://www.cmpe.boun.edu.tr/~sen/publications.htm
>
> Moreover, I have formalized LLVM IR in Haskell/uuagc (Utrecht
> University Attribute Grammar Compiler) and implemented a first version
> of a SMT BMC for concurrent c programs at the LLVM IR level. I
> describe this framework in my MSc. thesis: A Framework for Formal
> Verification of Concurrent Software which is accessible here:
> http://igitur-archive.library.uu.nl/student-theses/2012-0925-200740/UUindex.html
>
> Thank you.
>
> Kind regards,
> Marcelo
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev