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
>