[llvm-dev] Question about Formal Verification

[John Criswell via llvm-dev]

Dear Scott,

You may want to look at the SMACK project 
(http://soarlab.org/2014/05/smack-decoupling-source-language-details-from-verifier-implementations/). 
SMACK converts LLVM IR into the Boogie verification language.  The 
abstract states that they are building verification tools upon SMACK.

Regards,

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
http://www.cs.rochester.edu/u/criswell

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