llvm dev - Jan 2013 - [LLVMdev] Publication Generation of TLM Testbenches Using Mutation Testing

Dear all,

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

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

Very interesting, thanks for the forward!  If you're interested in having a
link posted on llvm.org, please email the llvmdev mailing list.

-Chris

On Jan 30, 2013, at 9:42 AM, Marcelo Sousa <marceloabsousa at gmail.com>
wrote:
> Dear all,
> 
> 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