[LLVMdev] Type-based analysis for LLVM IR

[Roel Jordans]

Hi Marcello,

It sounds like Vellvm could be interesting for you to consider

http://www.cis.upenn.edu/~jianzhou/Vellvm/

Regards,
  Roel

On 03/04/13 15:21, Marcelo Sousa wrote:
> 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