Directed graphs: circuits, maximal subtrees, paths, DAGs.
- C. Blaudeau added a topological sort to the digraph library, defined
on computable acyclic digraphs. A couple of changes have been made to
split the paths.pvs and dag.pvs for the two definitions of
digraphs. The main theory
c_topological_sortrevolves around a visit function that does a depth-first search of the graph, using a marking system (none, temporary, permanent)
| Theorem | Location | PVS Name | Contributors |
|---|
- Andreia Avelar Borges, University of Brasilia, Brazil
- Jon Sjogren, Department of Defense, USA
- Kristin Rozier, NASA, USA
- Ricky Butler, NASA, USA
- César Muñoz, NASA, USA
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- Thomas Norris
- Clément Blaudeau, EPFL, Switzerland and Ecole Polytechnique, France
- César Muñoz, NASA, USA
