The formal verification of concurrent software often amounts to analyzing some combinatorial state space, such as a directed graph. As time scales shrink and numbers of processes increases, the sizes of these directed graphs explode. Despite existing state space reduction techniques, this combinatorial explosion often renders industrial validation of concurrent software incomplete in practice; system designers often must accept either a certain level of risk or reduced performance from a simplified design. A “directed space,” a topological space equipped with some structure of time, represents the limit of ever more intricate directed graphs representing ever finer observations in time. Classical algebraic topology gives tractable methods for classifying reasonable spaces, irrespective of size, typically up to continuous deformation. Some forms of critical system behavior remain unchanged under continuous deformations respecting time flow. An appropriate "directed algebraic topology" thus provides a naturally geometric program semantics and a convenient setting for circumventing combinatorial explosion in validating concurrent programs.

We introduce basic ideas from directed algebraic topology (not assuming any prior familiarity with classical algebraic topology) and show how calculations of suitable invariants on directed spaces, some of which were jointly developed with Eric Goubault and Emmanuel Haucourt from the French Atomic Energy Commission, can reveal coordination problems in concurrent software. We also compare our directed topological approach with traditional model- checking and sketch applications of directed algebraic topology to rewriting theory (time-permitting).