Acknowledgments
Introduction
Preliminaries
Separation Logic
Ghost State
The Keyset Resource Algebra
The Edgeset Framework for Single-Copy Structures
The Flow Framework
Verifying Single-Copy Concurrent Search Structures
Verifying Multicopy Structures
The Edgeset Framework for Multicopy Structures
Reasoning about Non-Static and Non-Local Linearization Points
Verifying the LSM DAG Template
Proof Mechanization and Automation
Related Work, Future Work, and Conclusion
Bibliography
Authors' Biographies.