categories and formal verification

categories and formal verification

[David CHEMOUIL]

Dear colleagues,


Some colleagues of mine and myself are currently investigating categorical
approaches to component-based development for software, in the spirit of J.
L. Fiadeiro's work or of the coalgebra community.

Being new to the discipline, it also implies for them quite some work in
basic CT itself. Hence, they're looking for some kind of reason making this
tedious process worth enduring. Elegance of CT is one such reason, Goguen's
or Ehrig's arguments in a few articles are others.

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?).

I couldn't find convincing examples, even in Goguen's Manifesto, so I
wondered whether you had good arguments and/or references to such convincing
work, that would give them the impetus to continue studying this topic.

Regards,

dc
-- 
David CHEMOUIL
ONERA/DTIM
http://www.onera.fr/staff/david-chemouil


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: categories and formal verification

[Vaughan Pratt]

David CHEMOUIL wrote:
> 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?).

When deadlocks are modeled in the geometric manner of Papadimitriou's
"Concurrency Control," one can apply categorical methods as in

         @InProceedings(
Pr91a,  Author="Pratt, V.R.",
         Title="Modeling Concurrency with Geometry",
         Booktitle="Proc. 18th Ann. ACM Symposium on Principles of
         Programming Languages", Pages="311-322",
         Month=Jan, Year=1991)

downloadable as http://boole.stanford.edu/pub/cg.pdf

This paper modeled concurrent phenomena via higher dimensional
transitions, formalized by directed or monoidal (as opposed to
groupoidal) homotopy, nowadays called dihomotopy, represented in the
case of my paper using n-categories.  Eric Goubault and Thomas Jensen
subsequently developed this notion in a homological framework,
presenting "Homology of higher-dimensional automata" at CONCUR'92.
Goubault then founded the GETCO (GEometric and Topological COmputation)
series of conferences on higher dimensional automata and related
geometric models, the seventh of which was held in San Francisco in
2005.  Since then other geometric models besides n-categories have been
used, although Philippe Gaucher has stuck with the n-category approach
more faithfully even than myself (following a suggestion of Rob van
Glabbeek I've drifted over to cubical complexes, the category of which
is neatly definable as the topos Set^FinBip where FinBip is the category
of finite bipointed sets---actually the free such suffice).

Since the above POPL paper has 99 citations I suggest following those
links forward in time (backward along the links) to see how the
categorical aspects have been applied in the intervening 18 years and
how the thinking along that homological/dihomotopic line has developed.

Verification should not be thought of as simply manipulation of logical
formulas, but should take into account the known algorithms for the data
structures arising in the programs being verified.  In the case of
concurrent programs, especially for phenomena such as deadlock, higher
dimensional automata supply core data structures for the concept.  When
the essence of deadlock is geometric, translating the concepts into a
logical language and applying decision methods tailored to logic tends
to hide the wood with the trees.

Vaughan Pratt


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: categories and formal verification

[Barbara Koenig]

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/ ]

Re: categories and formal verification

[Bas Spitters]

We used monads and applicative functors to verify an implementation real=20
integration. We found CT to be convenient in the process:

A computer verified, monadic, functional implementation of the integral.
Russell O'Connor, Bas Spitters
http://arxiv.org/abs/0809.1552
Abstract: We provide a computer verified exact monadic functional=20
implementation of the Riemann integral in type theory. Together with previo=
us=20
work by O=E2=80=99Connor, this may be seen as the beginning of the realizat=
ion of=20
Bishop=E2=80=99s vision to use constructive mathematics as a programming la=
nguage for=20
exact analysis.




Best regards,

Bas

On Tuesday 08 September 2009 09:20:52 David CHEMOUIL wrote:
> Dear colleagues,
>
>
> Some colleagues of mine and myself are currently investigating categorical
> approaches to component-based development for software, in the spirit of =
J.
> L. Fiadeiro's work or of the coalgebra community.
>
> Being new to the discipline, it also implies for them quite some work in
> basic CT itself. Hence, they're looking for some kind of reason making th=
is
> tedious process worth enduring. Elegance of CT is one such reason, Goguen=
's
> or Ehrig's arguments in a few articles are others.
>
> 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?).
>
> I couldn't find convincing examples, even in Goguen's Manifesto, so I
> wondered whether you had good arguments and/or references to such
> convincing work, that would give them the impetus to continue studying th=
is
> topic.
>
> Regards,
>
> dc


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]