[llvm-dev] Question about Formal Verification

[Andrew Santosa via llvm-dev]

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,
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/20160210/89fdfefb/attachment.html>