Openproofs:Current events

From Openproofs

2009-10-16

The CVC3 license is now FLOSS (it's a straight BSD license). This is great news. The CVC3 authors intended for CVC3 to be open source software, but the lawyers added some non-standard terms.

2009-09-04

The Auto-DESTDIR package is now in Fedora's online repository (Fedora 10, the current Fedora 11, and the upcoming Fedora 12). This will hopefully make it easier to package and distribute formal proof tools.

2009-08-31

"Where Have You Gone, Bell Labs?" (BusinessWeek) isn't specifically about open proofs, but it does point to the need for more investment in work with longer-term horizons.

2009-08-13

Open Proofs presentation given at Mil-OSS.

The Auto-DESTDIR package has just been released to the public. This makes it easier to package programs, which in turn makes it easier to get tools into the hands of real end-users.

2009-08-01

Proof General package approved. See https://bugzilla.redhat.com/show_bug.cgi?id=484049. Package is already in Fedora rawhide, will be migrating back to Fedora 10, 11.

2009-07-06

IPPR Report Includes a related recommendation. The report "Shared Responsibilities: A national security strategy for the UK" by the Institute for Public Policy Research (ippr) Commission on National Security in the 21st Century (30 June 2009, ISBN 9781860303258) includes "Recommendation 60: The Government should also approach the European Commission and the incoming Swedish Presidency to sponsor a programme for the creation of a range of secure and reliable standard software modules (such as simple operating systems, database management systems and graphical user interfaces). These modules should be developed using formal methods and be made available free of charge through an open source licence to encourage their widespread use." The entire report has a small cost, but a summary (including its recommendations) can be obtained at no charge without registering. DWheeler

2009-06-17

Draft ACL2 package. See https://www.openproofs.org/packages/acl2/, and the Review Request (https://bugzilla.redhat.com/show_bug.cgi?id=506567). (The latter has some details one would be best knowing. The package is being built again at the moment, so the SPEC and SRPM files may be slightly out of sync with the RPMs - this will be fixed later.) ADunn

2009-06-05

SPARK released as open source software!. SPARK GPL Edition has just been released by Praxis as open source software (using the GPL). SPARK is a sub+superset of Ada for developing provable programs: Programs written in SPARK can be compiled by a standard Ada compiler (including the GPL'ed GNAT), and they can also be processed by Praxis' SPARK tools to prove properties about them. Praxis just released its SPARK tools as open source software (GPL license) in June 2009.

This means that Tokeneer is now an open proof. To be an open proof, a program's implementation, proofs, and required tools have to be open source software. Tokeneer is a sample proven program written in SPARK, released as open source software. Its proofs were also released as open source software. There are two kinds of tools required: An Ada compiler (the GPL'ed GNAT meets this), and SPARK proving tools (the Praxis SPARK GPL edition meets this).

This is excellent!! Please help us package SPARK for common platforms so that it's easier to install. DWheeler

2009-05-22

You haven't seen much from me (Alan Dunn) lately because I'm actually trying to use some of these formal methods tools. I'm trying to analyze parts of Linux-PAM (specifically pam_unix) using Frama-C, the packaging of which was the goal of some of my previous packaging efforts (eg: APRON). We're not quite there yet (there are definitely some issues with the APRON package, and no-one has reviewed it yet), but this way something can be done while approaching the packaging side simultaneously. ADunn

2009-05-01

APRON draft package complete. SRPM and spec file locations here with the review request - sorry for the delay! ADunn

2009-04-14

APRON package nearing completion. ADunn

2009-04-08

mmm approved (see previous link). Proof General still needs x-symbol to be packaged, but there are modifications to the Proof General version, which means that I need to figure out exactly what modifications there are and try to extract them. Packaging Coq 8.2 - almost done. ADunn

2009-04-07

Packaged mmm for use with the Proof General package. see: https://bugzilla.redhat.com/show_bug.cgi?id=494647. ADunn

2009-04-06

Proof General review ongoing (though it may need some modification), again, see https://bugzilla.redhat.com/show_bug.cgi?id=484049. ADunn

2009-04-02

New version of MLGMPIDL package. Now packaging APRON. Encountering many of the same difficulties as for MLGMPIDL - this is because developers often don't think of the fact that for packaging software it is useful to have more options for include, library, binary placement (eg: some platforms use /usr/lib64 for certain libraries -> should not expect (something)/lib at all points...) I know I wouldn't have thought of issues like this before I started packaging programs. ADunn

2009-04-01

Package for MLGMPIDL recently completed (https://bugzilla.redhat.com/show_bug.cgi?id=491712), only to discover (4/1) that the version downloaded from the official (?) site (http://www.inrialpes.fr/pop-art/people/bjeannet/mlxxxidl-forge/mlgmpidl/index.html) was not as recent as needed! (Missing Mpfrf module used in APRON).

Proof General package still needs review. ADunn

2009-03-19

We now have an SSL certificate. When you log in to edit wiki pages, please use https: and not http: (to prevent password sniffing).

2009-03-18

The Open Proofs site is up and ready! We don't yet have our own cert installed, so if you log in with SSL (recommended for editing), you'll get a complaint from your browser. We intend to fix this soon.

Of the 23 "most promising" tools we initially identified, we have about 40% packaged and part of Fedora's standard repository, another 30% in process, and 40% to start. The key reason for packaging into a standard repository is that users can easily install the program - you can just add a checkmark to the name, and it'll be downloaded and installed (including all dependencies). Also, packaging in Free / Libre / Open Source Software (FLOSS) systems is the integration step that resolves many standard integration problems: integrate programs more cleanly, update older libraries, verify that the program is actually FLOSS, and so on.

2009-02-04

Proof General potential package for Fedora up (http://www.phy.duke.edu/~amd34/pg/). See review status at https://bugzilla.redhat.com/show_bug.cgi?id=484049. ADunn