[llvm-dev] Question about Formal Verification

[Scott Santucci via llvm-dev]

I'd just like to thank everyone who replied on this; the suggestions and
resources are very helpful!

~Scott

On Tue, Feb 9, 2016 at 8:38 PM, Andrew Santosa <santosa_1999 at yahoo.com>
wrote:

> LLBMC http://llbmc.org uses bounded model checking technique to find
> errors in LLVM IR.
> Model checking is essentially search, and since LLBMC is bounded, the
> search for errors is usually
> incomplete, hence the approach may not verify the entire program, however,
> it may be good
> enough to find interesting errors.
>
> Best wishes,
> Andrew
>
>
> On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev <
> llvm-dev at lists.llvm.org> wrote:
>
>
> Hello, all,
> My name is Scott Santucci and I'm a software developer kicking around
> various wild ideas. (I wish I had something more interesting to say about
> myself than that, but nothing comes to mind; my day job is in SQL and Java,
> nothing to do with LLVM.)
> I am wondering whether anyone has tried using LLVM to apply formal
> verification to program code. I'm thinking about trying to develop tools
> that would leverage LLVM to check whether a program meets a design
> specification -- conservatively, I suppose, since knowing the full behavior
> of arbitrary programs is probably reducible to the halting problem but to
> my knowledge one can always come up with a more constrained check for which
> failure merely leaves unknowns rather than trying to resolve
> halting-problem-equivalent questions. Anyway, I figure I should start by
> finding out if there is prior work in that area. If this isn't the best
> place to ask, feel free to direct me elsewhere.
> Thanks,
> Scott
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20160229/b2a75e86/attachment-0001.html>