Deutsch Schorr Waite (Q40551)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry GraphMarkingIBP
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Deutsch Schorr Waite |
AFP entry GraphMarkingIBP |
Statements
Viorel Preoteasa
0 references
Ralph-Johan Back
0 references
The verification of the Deutsch-Schorr-Waite graph marking algorithm is used as a benchmark in many formalizations of pointer programs. The main purpose of this mechanization is to show how data refinement of invariant based programs can be used in verifying practical algorithms. The verification starts with an abstract algorithm working on a graph given by a relation next on nodes. Gradually the abstract program is refined into Deutsch-Schorr-Waite graph marking algorithm where only one bit per graph node of additional memory is used for marking.
0 references
28 May 2010
0 references
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement (English)
0 references
