Re: categories and formal verification

[Vaughan Pratt <pratt@cs.stanford.edu>]

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