-
Notifications
You must be signed in to change notification settings - Fork 8
/
meta.yml
112 lines (94 loc) · 3.57 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
---
fullname: Tarjan and Kosaraju
shortname: tarjan
organization: coq-community
opam_name: coq-mathcomp-tarjan
community: true
action: true
coqdoc: false
synopsis: Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
description: |-
This development contains formalizations and correctness proofs, using Coq and the Mathematical
Components library, of algorithms originally due to Kosaraju and Tarjan for finding strongly
connected components in finite graphs. It also contains a verified implementation of topological
sorting with extended guarantees for acyclic graphs.
publications:
- pub_title: Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
pub_url: https://hal.inria.fr/hal-01906155
pub_doi: 10.4230/LIPIcs.ITP.2019.13
- pub_title: Formally-Proven Kosaraju's algorithm
pub_url: https://hal.inria.fr/hal-01095533
authors:
- name: Cyril Cohen
initial: true
- name: Jean-Jacques Lévy
initial: true
- name: Karl Palmskog
- name: Laurent Théry
initial: true
maintainers:
- name: Cyril Cohen
nickname: CohenCyril
- name: Karl Palmskog
nickname: palmskog
opam-file-maintainer: Cyril Cohen <cyril.cohen@inria.fr>
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
file: CeCILL-B
supported_coq_versions:
text: '8.16 or later'
opam: '{>= "8.16"}'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{>= "2.0"}'
description: |-
[MathComp ssreflect 2.0 or later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
description: |-
[MathComp fingroup](https://math-comp.github.io)
- opam:
name: coq-hierarchy-builder
version: '{>= "1.4.0"}'
description: |-
[Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.4.0 or later
tested_coq_opam_versions:
- version: '2.0.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.17'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.16'
repo: 'mathcomp/mathcomp-dev'
namespace: mathcomp.tarjan
keywords:
- name: strongly connected components
- name: topological sorting
- name: Kosaraju
- name: Tarjan
- name: acyclicity
- name: graph theory
categories:
- name: Computer Science/Graph Theory
documentation: |-
## Main files
### Extra library files
* `bigmin.v`: extra library to deal with `\min(i in A) F i`
* `extra.v`: naive definitions of strongly connected components and various basic extentions of mathcomp libraries on paths and fintypes
* `acyclic.v`: definition of acyclic graphs and proof that acyclicity can be determined by knowing strongly connected components
### Proof of Kosaraju strongly connected component algorithm
* `kosaraju.v`: proof of topological sorting and Kosaraju connected component algorithm
* `acyclic_tsorted.v`: properties of topological sorting in acyclic graphs
### Proofs of Tarjan strongly connected component algorithm (independent from each other)
* `tarjan_rank.v`: proof with rank
* `tarjan_rank_bigmin.v`: same proof but with a `\min_` instead of multiple inequalities on the output rank
* `tarjan_num.v`: same proof as `tarjan_rank_bigmin.v` but with serial numbers instead of ranks
* `tarjan_nocolor.v`: new proof, with ranks and without colors, less fields in environement and less invariants, preconditions and postconditions.
* `tarjan_nocolor_optim.v`: same proof as `tarjan_nocolor.v`, but with the serial number field of the environement restored, and passing around stack extensions as sets
---