[llvm-dev] Question about Formal Verification

[Mueller-Roemer, Johannes Sebastian via llvm-dev]

I don’t know if there is any work on using LLVM *for* formal verification, but there is work on formal verification of LLVM (passes): https://www.cis.upenn.edu/~stevez/vellvm/

--
Johannes S. Mueller-Roemer, MSc
Wiss. Mitarbeiter - Interactive Engineering Technologies (IET)

Fraunhofer-Institut für Graphische Datenverarbeitung IGD
Fraunhoferstr. 5  |  64283 Darmstadt  |  Germany
Tel +49 6151 155-606  |  Fax +49 6151 155-139
johannes.mueller-roemer at igd.fraunhofer.de  |  www.igd.fraunhofer.de

From: llvm-dev [mailto:llvm-dev-bounces at lists.llvm.org] On Behalf Of Scott Santucci via llvm-dev
Sent: Monday, February 08, 2016 14:45
To: llvm-dev at lists.llvm.org
Subject: [llvm-dev] Question about Formal Verification


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/d98644e1/attachment-0001.html>