CVC3 is one of the better automated theorem provers. Given certain mathematical assertions, it can in many cases prove that certain claims follow from them. Some tools that can prove properties about programs use CVC3 (and/or similar programs). For example, the Frama-C Jessie plug-in for C and Krakatoa for Java use Why, which can build on one of several programs including CVC3.
Problem is, CVC’s license has historically been a problem. I understand that its authors intended for CVC3 to be Free/Libre/Open Source Software (FLOSS), but unfortunately, it was released with additional license clauses that resulted in yet another non-standard license. This was an unfortunate mistake; as I note in my essay on GPL-compatible licenses, it is absolutely critical to choose a standard FLOSS license when releasing FLOSS. In this case, the big problem was the addition of an “indemnification” clause that was really scary; to some, at least, it seemed to imply that if the CVC3 authors were sued, anyone who used or copied the program was obligated to pay their legal bills. Interpreted that way, no one wanted to touch the program… how could any user possibly know their risks? Fedora eventually ruled that this license was non-free (aka not FLOSS), and thus could not be included in Fedora. There was a less-serious problem that if you made a change to the program, you had to change the name… since the program couldn’t even compile without a change (at the time), this meant that you had to change the name almost instantly. There is a reason that people have converged on standard FLOSS licenses; if your lawyer says you need to add non-standard clauses, be wary, because the result may be that few people can use your program.
I’m delighted to report that this has a happy ending. CVC3’s license has just been changed to a straight BSD license - a well-known license that is universally acknowledged as being FLOSS. This means that there are no licensing problems for Linux distributions. Only about a day after he found this out, Jerry James has submitted a CVC3 package to Fedora. So, I expect that in a relatively short time we’ll see CVC3 available directly in common Linux distribution repositories.
I think this is a helpful step towards open proofs, which are cases where an implementation, its proofs, and the necessary tools are all FLOSS. Having a good tool like CVC3 to build on makes it easier to develop useful tools. My hope is to mature formal methods tools so that they can be more scaleable, applicable, and effective than they are today. It’s clear that a single little tool cannot possibly do the job; we need suites of tools that can work together. And this is a promising step in that direction.
path: /oss | Current Weblog | permanent link to this entry