From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from lists.gentoo.org ([140.105.134.102] helo=robin.gentoo.org) by nuthatch.gentoo.org with esmtp (Exim 4.60) (envelope-from ) id 1FvCGu-0006C1-Uw for garchives@archives.gentoo.org; Tue, 27 Jun 2006 12:02:25 +0000 Received: from robin.gentoo.org (localhost [127.0.0.1]) by robin.gentoo.org (8.13.7/8.13.6) with SMTP id k5RBxUiF001380; Tue, 27 Jun 2006 11:59:30 GMT Received: from anubis.medic.chalmers.se (anubis.medic.chalmers.se [129.16.30.218]) by robin.gentoo.org (8.13.7/8.13.6) with ESMTP id k5RBxSNY006223 for ; Tue, 27 Jun 2006 11:59:28 GMT X-Medic-Info: c15.44a11da0.0 EadBFjjsu0s0DNlQ nodot-helo dynamic-client Received: from localhost (wavelan105.doc.ic.ac.uk [146.169.25.105]) by mail.chalmers.se (Postfix) with ESMTP id 3F82330FA1 for ; Tue, 27 Jun 2006 13:59:28 +0200 (CEST) Date: Tue, 27 Jun 2006 14:00:46 +0200 From: Alexandre Buisse To: gentoo-science@lists.gentoo.org Subject: Re: [gentoo-science] sci-proof Message-ID: <20060627120046.GD24355@ubik> References: <20060626161440.38076.qmail@web31715.mail.mud.yahoo.com> <44A0BF58.8080305@cesmail.net> Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-science@gentoo.org Reply-to: gentoo-science@lists.gentoo.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="UfEAyuTBtIjiZzX6" Content-Disposition: inline In-Reply-To: <44A0BF58.8080305@cesmail.net> X-Operating-System: Linux 2.6.17-ubik i686 User-Agent: Mutt/1.5.11 X-Archives-Salt: c1569d84-6f86-47e2-b481-95645f366d7d X-Archives-Hash: 6627062d516555c07aeed7e5de0d2a8b --UfEAyuTBtIjiZzX6 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-Transfer-Encoding: quoted-printable On Tue, Jun 27, 2006 at 12:57:12 +0200, M. Edward (Ed) Borasky wrote: >=20 >=20 > C Y wrote: > > I'm sure I missed a few. Anyway, certainly enough to start :-). > > =20 > Well -- if we're going to get *that* specialized , how about adding > "maria" (which is in Debian -- it's a Petri net reachability analyzer), > the PEPA Workbench (in Java ... most likely not in Debian), PRISM > (http://www.cs.bham.ac.uk/~dxp/prism/download.php) and PDQ > (http://perfdynamics.com). > > > Seriously, though, PRISM is a quite useful and magnificent piece of > open-source work. Nearly all the other software in this domain > (probabilistic model checking and Markov process modeling) is either > commercial or tied up in an "academic (non-commercial)" non-free license > of some kind. Well, model checking is outside the (admittedly very narrow) scope of software I'm interested/skilled in, which deals mostly with proof assistant. If enough interest is shown, I could try to add them, but after we are done with the proof assistants (another possibility would of course be for you to become a dev yourself and maintain them :)). Regards, /Alexandre --UfEAyuTBtIjiZzX6 Content-Type: application/pgp-signature Content-Disposition: inline -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.3 (GNU/Linux) iD8DBQFEoR3twx9vvAARv2sRAke8AJwL6yl0+tw3E/pq3dVp25uNhkrPrQCffccl TkKFt4L0pzfbf6x0iPdgkZE= =V+4B -----END PGP SIGNATURE----- --UfEAyuTBtIjiZzX6-- -- gentoo-science@gentoo.org mailing list