| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
| Title: | Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement |
| Author: | Viorel Preoteasa and Ralph-Johan Back |
| Submission date: | 2010-05-28 |
| Abstract: | 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. |
| Change history: | [2012-01-05]: Updated for the new definition of data refinement and the new syntax for demonic and angelic update statements |
| BibTeX: |
@article{GraphMarkingIBP-AFP,
author = {Viorel Preoteasa and Ralph-Johan Back},
title = {Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement},
journal = {Archive of Formal Proofs},
month = may,
year = 2010,
note = {\url{http://afp.sf.net/entries/GraphMarkingIBP},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | DataRefinementIBP |
| Status: [ok] | This is the development version, revision 4b34a59339a6, of this entry, generated for Isabelle revision 90ba620333d0. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|