Announcement: LLBMC Version 2012.1 available

113 views
Skip to first unread message

carsten

unread,
Feb 6, 2012, 9:10:52 PM2/6/12
to LLBMC
***
* LLBMC: The Low-Level Bounded Model Checker
* for C (and C++) programs is now available!
* Version 2012.1, http://llbmc.org
***

We are very pleased to announce that LLBMC, a bug-finding tool for
C (and, to some extent, C++) programs, is now available.

LLBMC is a high-precision static analyzer implementing a technique
called "Bounded Model Checking". LLBMC is based on LLVM and can
detect errors such as:

- Illegal memory accesses (e.g., buffer overflows)
- Integer overflows
- Division by zero
- Invalid bit shifts
- Double frees

For more information and to download LLBMC see http://llbmc.org.

pini

unread,
Apr 12, 2012, 4:56:13 PM4/12/12
to ll...@googlegroups.com

LLBMC seems a very interesting tool for static checking. I particularly like the language-agnostic approach of operating over the LLVM IR.
Are you planning on releasing LLBMC source code as well?

Best regards.
 

Marko Schütz-Schmuck

unread,
May 6, 2012, 12:56:04 PM5/6/12
to ll...@googlegroups.com
 
That  would be my question also: are you planning to release LLBMC source code?

Best regards,

Marko

Florian Merz

unread,
May 16, 2012, 10:31:30 AM5/16/12
to LLBMC
Hi pini, hi Marko,

a source code release is not planned in the near futurue and we have
also not yet made a final decision on releasing LLBMC's source code at
all.

Best regards,
Florian Merz

On 6 Mai, 18:56, Marko Schütz-Schmuck <markoschu...@googlemail.com>
wrote:
> On Thursday, April 12, 2012 4:56:13 PM UTC-4, pini wrote:
>
> > ***
> >> *   LLBMC: The Low-Level Bounded Model Checker
> >> *   for C (and C++) programs is now available!
> >> *   Version 2012.1,http://llbmc.org
> >> ***
>
> >> We are very pleased to announce that LLBMC, a bug-finding tool for
> >> C (and, to some extent, C++) programs, is now available.
>
> >> LLBMC is a high-precision static analyzer implementing a technique
> >> called "Bounded Model Checking". LLBMC is based on LLVM and can
> >> detect errors such as:
>
> >> - Illegal memory accesses (e.g., buffer overflows)
> >> - Integer overflows
> >> - Division by zero
> >> - Invalid bit shifts
> >> - Double frees
>
> >> For more information and to download LLBMC seehttp://llbmc.org.

Paul Brauner

unread,
May 16, 2012, 11:32:27 AM5/16/12
to ll...@googlegroups.com


On Wednesday, May 16, 2012 4:31:30 PM UTC+2, Florian Merz wrote:
Hi pini, hi Marko,

a source code release is not planned in the near futurue and we have
also not yet made a final decision on releasing LLBMC's source code at
all.


It would be really really great if you did!

Paul

Marko Schütz-Schmuck

unread,
May 17, 2012, 4:56:06 PM5/17/12
to ll...@googlegroups.com
Dear Florian,

excuse my skepticism/pessimism it might be completely unjustified in this case: but without access to the source code under a proper FLOSS license, this could be a project that starts out in academia, builds a community, and then is lost to that same community because either

  1. the research project behind it ends and/or the people behind it move on to new projects, or
  2. the source code end up as an asset of some company that builds products and offers services around it, based on the work (feedback/testing) of the community
In either case the community participants loose their time and effort. So, I strongly suggest licensing the source code with a FLOSS license.

Best regards,

Marko

Florian Merz

unread,
May 18, 2012, 4:17:13 AM5/18/12
to LLBMC
Hi Marko,

we do know the pros and cons of open sourcing LLBMC, and we're
discussing the issue regularly, we just haven't made a decision on
this yet. Bear with us please.

Regards,
Florian

On May 17, 10:56 pm, Marko Schütz-Schmuck
<markoschu...@googlemail.com> wrote:
> Dear Florian,
>
> excuse my skepticism/pessimism it might be completely unjustified in this
> case: but without access to the source code under a proper FLOSS license,
> this could be a project that starts out in academia, builds a community,
> and then is lost to that same community because either
>
>    1. the research project behind it ends and/or the people behind it move
>    on to new projects, or
>    2. the source code end up as an asset of some company that builds

Marko Schütz-Schmuck

unread,
Dec 2, 2013, 7:17:37 AM12/2/13
to ll...@googlegroups.com
Dear Florian,

it seems you have effectively reached a decision on whether to release the source code under a FLOSS license or how are we supposed to interpret the fact that after over one and a half years there is still no source code?

Best regards,

Marko
Reply all
Reply to author
Forward
0 new messages