Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement (Q7361598)
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 | Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement |
AFP entry GraphMarkingIBP |
Statements
28 May 2010
0 references
Viorel Preoteasa
0 references
Ralph-Johan Back
0 references
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement (English)
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
