[LLVMdev] Publication Generation of TLM Testbenches Using Mutation Testing

[Marcelo Sousa]

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