@conference {PP11,
	title = {Model Checking a Decentralized Storage Deduplication Protocol},
	booktitle = {Fast Abstract in Latin-American Symposium on Dependable Computing},
	year = {2011},
	month = {April},
	pages = {1},
	address = {S{\~a}o Jos{\'e} dos Campos, Brazil},
	abstract = {<p>Deduplication of live storage volumes in a cloud computing environment is better done by post-processing: by delaying discovery and removal of duplicate data after I/O requests have been concluded, impact in latency can be minimized. When compared to traditional deduplication in backup systems, which can be done in-line and in a centralized fashion, distribution and concurrency lead to increased complexity. This paper outlines a deduplication algorithm for a typical cloud infrastructure with a common storage pool and summarizes how model-checking with the TLA+ toolset was used to uncover and correct some subtle concurrency issues.</p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/jtpaulo/files/pp09.pdf},
	author = {Jo{\~a}o Paulo and Jos{\'e} Orlando Pereira}
}