Re: categories and formal verification

[Barbara Koenig <barbara_koenig@uni-due.de>]

Dear David,

David CHEMOUIL <David.Chemouil@onera.fr> 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 provide
> support in *verifying* things about systems under study (e.g what does CT
> approaches bring to check the absence of deadlocks in a concurrent system?).

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 

**********************************************************************

Paolo Baldan, Andrea Corradini, and Barbara König. 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önig. 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.pdf

Salil Joshi and Barbara König. 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önig. 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/ ]