[LLVMdev] secure virtual architecture / safecode

[John Regehr]

Hi Vikram-

Certainly I'm far from being an expert on this topic.  However, many of 
the theories supported by SMT-LIB seem useful, such as arrays, bitvectors, 
etc:

   http://combination.cs.uiowa.edu/smtlib/theories.html

Also, SMT has a uniform input format and so different solvers could be 
tried out at little cost.

In the slightly longer term, the ability to deal with quantifiers would be 
nice to help sort out lightweight verification problems of the sort that 
ESC-Java supports.  This seems to be about the right level of 
specification for many types of problems.

John



On Fri, 27 Mar 2009, Vikram S. Adve wrote:

> SMT solvers seem more general-purpose than we need.  We just need an
> ILP solver of some kind (Omega, PIP, TaPAS, ...) for almost all uses I
> can think of.  Do you want to do more powerful symbolic analysis for
> some purpose?
>
> --Vikram
> Associate Professor, Computer Science
> University of Illinois at Urbana-Champaign
> http://llvm.org/~vadve
>
>
>
> On Mar 27, 2009, at 12:08 PM, John Regehr wrote:
>
>> On Wed, 25 Mar 2009, Vikram S. Adve wrote:
>>
>>> We do have a static array bounds checking algorithm based on the
>>> Omega
>>> integer programming library, but it is not hugely effective.  I think
>>> this can be strengthened a *lot*.
>>
>> I should add that I would be interested in helping with hooking a good
>> decision procedure into LLVM.  This will be useful far beyond array
>> bounds
>> check elimination.
>>
>> What is the current thinking?  SMT solver?
>>
>> John
>> _______________________________________________
>> LLVM Developers mailing list
>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>