llvm dev - Feb 2016 - 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/9bf25747/attachment.html>

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>

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>

LLBMC http://llbmc.org uses bounded model checking technique to find errors in
LLVM IR.Model checking is essentially search, and since LLBMC is bounded, the
search for errors is usuallyincomplete, hence the approach may not verify the
entire program, however, it may be goodenough to find interesting errors.

Best wishes,Andrew
 

    On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev <llvm-dev
at lists.llvm.org> 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


  
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20160210/89fdfefb/attachment.html>

I'd just like to thank everyone who replied on this; the suggestions and
resources are very helpful!

~Scott

On Tue, Feb 9, 2016 at 8:38 PM, Andrew Santosa <santosa_1999 at yahoo.com>
wrote:
> LLBMC http://llbmc.org uses bounded model checking technique to find
> errors in LLVM IR.
> Model checking is essentially search, and since LLBMC is bounded, the
> search for errors is usually
> incomplete, hence the approach may not verify the entire program, however,
> it may be good
> enough to find interesting errors.
>
> Best wishes,
> Andrew
>
>
> On Monday, 8 February 2016, 21:54, Scott Santucci via llvm-dev <
> llvm-dev at lists.llvm.org> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20160229/b2a75e86/attachment-0001.html>