[llvm-dev] Question about Formal Verification
Scott Santucci via llvm-dev
llvm-dev at lists.llvm.org
Mon Feb 29 16:18:49 PST 2016
I'd just like to thank everyone who replied on this; the suggestions and
resources are very helpful!
On Tue, Feb 9, 2016 at 8:38 PM, Andrew Santosa <santosa_1999 at yahoo.com>
> 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,
> 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.
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the llvm-dev