<div dir="ltr"><div>I'd just like to thank everyone who replied on this; the suggestions and resources are very helpful!</div><div><br></div><div>~Scott</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 9, 2016 at 8:38 PM, Andrew Santosa <span dir="ltr"><<a href="mailto:santosa_1999@yahoo.com" target="_blank">santosa_1999@yahoo.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div style="color:rgb(0,0,0);font-family:HelveticaNeue,Helvetica Neue,Helvetica,Arial,Lucida Grande,Sans-Serif;font-size:12px;background-color:rgb(255,255,255)"><div dir="ltr">LLBMC <a href="http://llbmc.org" target="_blank">http://llbmc.org</a> uses bounded model checking technique to find errors in LLVM IR.</div><div dir="ltr">Model checking is essentially search, and since LLBMC is bounded, the search for errors is usually</div><div dir="ltr">incomplete, hence the approach may not verify the entire program, however, it may be good</div><div dir="ltr">enough to find interesting errors.<br></div><div dir="ltr"><br></div><div dir="ltr">Best wishes,</div><div dir="ltr">Andrew<br></div><div><span></span></div> <div><br><br></div><div style="display:block"> <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><div class="h5"> <div dir="ltr"><font face="Arial" size="2"> On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>> wrote:<br></font></div>  <br><br> </div></div><div><div><div class="h5"><div><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></div></div><span>_______________________________________________<br>LLVM Developers mailing list<br><a href="mailto:llvm-dev@lists.llvm.org" target="_blank">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></span></div>  </div> </div>  </div></div></div></blockquote></div><br></div>