[llvm-dev] Question about Formal Verification

[Scott Santucci via llvm-dev]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20160208/9bf25747/attachment.html>