From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5129 Path: news.gmane.org!not-for-mail From: Barbara Koenig Newsgroups: gmane.science.mathematics.categories Subject: Re: categories and formal verification Date: Thu, 10 Sep 2009 18:18:50 +0200 Message-ID: Reply-To: Barbara Koenig NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1252685402 14801 80.91.229.12 (11 Sep 2009 16:10:02 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 11 Sep 2009 16:10:02 +0000 (UTC) To: David CHEMOUIL , Original-X-From: categories@mta.ca Fri Sep 11 18:09:54 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from [138.73.1.1] (helo=mailserv.mta.ca) by lo.gmane.org with esmtp (Exim 4.50) id 1Mm8h6-000712-2u for gsmc-categories@m.gmane.org; Fri, 11 Sep 2009 18:09:52 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Mm86E-0005dX-CD for categories-list@mta.ca; Fri, 11 Sep 2009 12:31:46 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5129 Archived-At: Dear David, David CHEMOUIL writes: > But, although my colleagues, are pretty convinced by the "constructive" > aspects of CT applied to such matters, they don't see how CT can provid= e > support in *verifying* things about systems under study (e.g what does = CT > approaches bring to check the absence of deadlocks in a concurrent syst= em?). If you search for a theorem of category theory that can be immediately applied to verification, then it will be difficult to find something. However, in our work on the verification of graph transformation we found it extremely helpful to work with category theory: it helps you in thinking about the subject matter, clarifying notions and especially it helped us to get shorter and more concise proofs (for instance correctness proofs, proofs of termination, etc.). Furthermore it is possible to develop generic verification procedures that work for a whole class of systems or develop tools which are parametric in the category (of course, it is then necessary to implement constructions for every specific category separately, but the overall effort is minimized.) Below I list a few of our papers on verification where category theory was helpful. It was not always entirely easy to sell the categorical background at verification-oriented conferences. So we sometimes trimmed it down to a minimum in the papers, although we worked with it much more extensively before. Barbara=20 ********************************************************************** Paolo Baldan, Andrea Corradini, and Barbara K=F6nig. A framework for the verification of infinite-state graph transformation systems. Information and Computation, 206:869-907, 2008. Paolo Baldan, Andrea Corradini, and Barbara K=F6nig. Unfolding graph transformation systems: Theory and applications to verification. Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, pages 16-36. Springer, 2008. LNCS 5065. http://www.ti.inf.uni-due.de/publications/koenig/festschrift-montanari.pd= f Salil Joshi and Barbara K=F6nig. Applying the graph minor theorem to the verification of graph transformation systems. In Prod. of CAV '08, pages 214-226. Springer, 2008. LNCS 5123. http://www.ti.inf.uni-due.de/publications/koenig/cav08.pdf Hartmut Ehrig and Barbara K=F6nig. Deriving bisimulation congruences in the DPO approach to graph rewriting. In Proc. of FOSSACS '04, pages 151-166. Springer, 2004. LNCS 2987. http://www.ti.inf.uni-due.de/publications/koenig/fossacs04.pdf [For admin and other information see: http://www.mta.ca/~cat-dist/ ]