<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">Dear Scott,<br>
<br>
You may want to look at the SMACK project
(<a class="moz-txt-link-freetext" href="http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/">http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/</a>).
SMACK converts LLVM IR into the Boogie verification language. The
abstract states that they are building verification tools upon
SMACK.<br>
<br>
Regards,<br>
<br>
John Criswell<br>
<br>
<br>
On 2/8/16 8:44 AM, Scott Santucci via llvm-dev wrote:<br>
</div>
<blockquote
cite="mid:CAGwF_kV-=UnUTyUQLnQk3yiLpfhPfjyFYXyHuJDtxO3Knp+7_g@mail.gmail.com"
type="cite">
<div dir="ltr">
<p>Hello, all,</p>
<p>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.)</p>
<p>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.</p>
<p>Thanks,<br>
Scott</p>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
LLVM Developers mailing list
<a class="moz-txt-link-abbreviated" href="mailto:llvm-dev@lists.llvm.org">llvm-dev@lists.llvm.org</a>
<a class="moz-txt-link-freetext" href="http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev">http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev</a>
</pre>
</blockquote>
<br>
<br>
<pre class="moz-signature" cols="72">--
John Criswell
Assistant Professor
Department of Computer Science, University of Rochester
<a class="moz-txt-link-freetext" href="http://www.cs.rochester.edu/u/criswell">http://www.cs.rochester.edu/u/criswell</a></pre>
</body>
</html>