[LLVMdev] Publication Generation of TLM Testbenches Using Mutation Testing

Marcelo Sousa marceloabsousa at gmail.com
Wed Jan 30 09:42:54 PST 2013

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:

Thank you.

Kind regards,

More information about the llvm-dev mailing list