search for: morrisett's

...objects. The SAFECode/SVA work developed a simple type checker that verified that the type-inference results returned by DSA are consistent (i.e., if DSA says that a memory object is used in a type-safe manner, then it is actually used in a type-safe manner). There is also some work by Greg Morrisett's group at Harvard at creating a verified type-checker for the SAFECode/SVA system. SAFECode/SVA papers can be found at http://sva.cs.illinois.edu/pubs.html. As far as formalisms for the LLVM IR, there is one from University of Pennsylvania (Santosh Nagarakatte, now at Rutgers, was involve...

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

Reed, Are you working on a grammar of the LLVM syntax or also on a full semantics? Steve Zdancewic's group at U. Penn. is working on a formal operational semantics for LLVM. It is partially complete and Greg Morrisett at Harvard is planning to build further on it. Regards, --Vikram Professor, Computer Science University of Illinois at Urbana-Champaign http://llvm.org/~vadve On Oct 20, 2011, at 11:56 AM, <llvmdev-request at cs.uiuc.edu> <llvmdev-request at cs.uiuc.edu> wrote: > Date: Thu, 2...

Hi John, John Regehr wrote: > PredicateSimplifier is a pretty interesting pass, but it doesn't look > like opt invokes it at any standard -Ox level, and so I assume that > llvm-gcc also does not use this pass? If that is right, I'm curious > about why this is the case -- does it simply not provide enough code > speedup to compensate for the increase in compile time? I

PredicateSimplifier is a pretty interesting pass, but it doesn't look like opt invokes it at any standard -Ox level, and so I assume that llvm-gcc also does not use this pass? If that is right, I'm curious about why this is the case -- does it simply not provide enough code speedup to compensate for the increase in compile time? Also, a colleague and I (we both teach advanced