Ion Chirica — Proof Artefacts
Why3 Proof Results
Generated by Why3.
Each obligation is discharged by one of three SMT solvers.
Times are in seconds. — ← Back to artifact page.
atd.ATD
✓ fully verified
| Obligation |
Alt-Ergo 2.5.2 |
CVC5 1.3.1 |
Z3 4.15.2 |
VC for n |
— | 0.01 | — |
VC for initWorld |
— | 0.03 | — |
VC for receive_message — split |
— | — | — |
| ↳ postcondition |
— | — | 0.01 |
VC for terminate_nd1 |
— | 0.03 | — |
VC for terminate_nd2 |
0.04 | — | — |
VC for send_message |
— | — | 0.02 |
VC for detect_termination |
— | 0.03 | — |
VC for initWorld'refn |
— | 0.02 | — |
VC for step'refn |
— | 0.04 | — |
safety |
— | 0.02 | — |
step_preserves_inv |
0.05 | — | — |
ewd998.EWD998
✓ fully verified
| Obligation |
Alt-Ergo 2.5.2 |
CVC5 1.3.1 |
Z3 4.15.2 |
VC for initWorld |
2.24 | — | — |
VC for initiate_probe |
0.79 | — | — |
VC for pass_token — split |
— | — | — |
| unfold inv |
— | — | — |
| ↳ VC for pass_token |
— | — | — |
| unfold inv in H |
— | — | — |
| ↳ VC for pass_token |
— | — | — |
| split_vc |
— | — | — |
| ↳ VC for pass_token |
— | — | 0.02 |
| ↳ VC for pass_token |
2.51 | — | — |
| split_vc |
— | — | — |
| ↳ VC for pass_token |
— | — | 0.02 |
| ↳ VC for pass_token |
0.90 | — | — |
| ↳ postcondition — split |
— | — | — |
| ↳ postcondition |
— | — | 0.02 |
| ↳ postcondition |
3.02 | — | — |
VC for sum_update — split |
— | — | — |
| ↳ assertion |
0.05 | — | — |
| ↳ assertion |
0.07 | — | — |
| ↳ postcondition |
— | — | 0.27 |
VC for send_message — split |
— | — | — |
| ↳ assertion — split |
— | — | — |
| ↳ assertion |
0.42 | — | — |
| ↳ assertion |
0.35 | — | — |
| ↳ VC for send_message |
— | — | 0.04 |
| unfold inv |
— | — | — |
| ↳ VC for send_message |
— | — | — |
| unfold inv in H |
— | — | — |
| split_vc |
— | — | — |
| ↳ VC for send_message |
0.06 | — | — |
| ↳ VC for send_message |
— | — | 1.97 |
| ↳ postcondition |
0.62 | — | — |
VC for receive_message — split |
— | — | — |
| ↳ assertion — split |
— | — | — |
| ↳ assertion |
0.32 | — | — |
| ↳ assertion |
0.28 | — | — |
| ↳ VC for receive_message |
— | — | 0.03 |
| unfold inv |
— | — | — |
| ↳ VC for receive_message |
— | — | — |
| unfold inv in H |
— | — | — |
| split_vc |
— | — | — |
| ↳ VC for receive_message |
0.08 | — | — |
| unfold safe in H |
— | — | — |
| ↳ VC for receive_message |
— | — | 0.25 |
| ↳ postcondition |
0.22 | — | — |
VC for deactivate — split |
— | — | — |
| ↳ postcondition |
0.08 | — | — |
| unfold inv in H |
— | — | — |
| split_vc |
— | — | — |
| ↳ postcondition |
3.01 | — | — |
VC for initWorldA'refn |
— | 0.02 | — |
VC for initWorldC'refn |
0.05 | — | — |
VC for stepA'refn |
0.03 | — | — |
VC for stepC'refn |
0.31 | — | — |