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:

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

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.

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