[LLVMdev] Type-based analysis for LLVM IR

[Marcelo Sousa]

I am interested in type-based verification of LLVM IR in the areas of
certified compilation and software verification. It seems to me that the
LLVM IR type system is rather informal in the sense that there is no paper
with a proper formalization of the type rules, and for example, a proof of
soundness for well-formedness of the code.
I would like to know if you are aware of any work in this direction for
LLVM IR so that I can compare with my own implementation.
Moreover, it would be valuable to get some feedback on suitable type-based
analysis that the LLVM community would like to have in the infrastructure.

Regards,
Marcelo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130403/b3ac0fdd/attachment.html>