[llvm-dev] Question about Formal Verification

John Criswell via llvm-dev llvm-dev at lists.llvm.org
Mon Feb 8 06:00:54 PST 2016

Dear Scott,

You may want to look at the SMACK project 
SMACK converts LLVM IR into the Boogie verification language.  The 
abstract states that they are building verification tools upon SMACK.


John Criswell

On 2/8/16 8:44 AM, Scott Santucci via llvm-dev 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

John Criswell
Assistant Professor
Department of Computer Science, University of Rochester

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20160208/8f4d5aae/attachment.html>

More information about the llvm-dev mailing list