[llvm-dev] Question about Formal Verification

Andrew Santosa via llvm-dev llvm-dev at lists.llvm.org
Tue Feb 9 17:38:18 PST 2016

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 usuallyincomplete, hence the approach may not verify the entire program, however, it may be goodenough 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,
LLVM Developers mailing list
llvm-dev at lists.llvm.org

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20160210/89fdfefb/attachment.html>

More information about the llvm-dev mailing list