<html><head></head><body><div style="color:#000; background-color:#fff; font-family:HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, Sans-Serif;font-size:12px"><div id="yui_3_16_0_1_1455067712794_21738" dir="ltr">LLBMC http://llbmc.org uses bounded model checking technique to find errors in LLVM IR.</div><div id="yui_3_16_0_1_1455067712794_21684" dir="ltr">Model checking is essentially search, and since LLBMC is bounded, the search for errors is usually</div><div id="yui_3_16_0_1_1455067712794_21914" dir="ltr">incomplete, hence the approach may not verify the entire program, however, it may be good</div><div id="yui_3_16_0_1_1455067712794_21882" dir="ltr">enough to find interesting errors.<br></div><div id="yui_3_16_0_1_1455067712794_21686" dir="ltr"><br></div><div id="yui_3_16_0_1_1455067712794_21685" dir="ltr">Best wishes,</div><div id="yui_3_16_0_1_1455067712794_21757" dir="ltr">Andrew<br></div><div id="yui_3_16_0_1_1455067712794_21662"><span></span></div> <div class="qtdSeparateBR"><br><br></div><div style="display: block;" class="yahoo_quoted"> <div style="font-family: HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, Sans-Serif; font-size: 12px;"> <div style="font-family: HelveticaNeue, Helvetica Neue, Helvetica, Arial, Lucida Grande, Sans-Serif; font-size: 16px;"> <div dir="ltr"><font face="Arial" size="2"> On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev <llvm-dev@lists.llvm.org> wrote:<br></font></div> <br><br> <div class="y_msg_container"><div id="yiv3193524127"><div dir="ltr"><div>Hello, all,</div><div>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.)</div><div>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.</div><div>Thanks,<br>Scott</div></div></div><br>_______________________________________________<br>LLVM Developers mailing list<br><a ymailto="mailto:llvm-dev@lists.llvm.org" href="mailto:llvm-dev@lists.llvm.org">llvm-dev@lists.llvm.org</a><br><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev" target="_blank">http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev</a><br><br><br></div> </div> </div> </div></div></body></html>