@inproceedings{windsor2017starling,
author = {Windsor, Matt and Dodds, Mike and Simner, Ben and Parkinson, Matthew},
title = {Starling: Lightweight Concurrency Verification with Views},
booktitle = {Computer Aided Verification 2017},
year = {2017},
month = {July},
abstract = {Modern program logics have made it feasible to verify the most complex concurrent algorithms. However, many such logics are complex, and most lack automated tool support. We propose Starling, a new lightweight logic and automated tool for concurrency verification. Starling takes a proof outline written in an abstracted Hoare-logic style, and converts it into proof terms that can be discharged by a sequential solver. Starling’s approach is generic in its structure, making it easy to target different solvers. In this paper we verify shared-variable algorithms using the Z3 SMT solver, and heap-based algorithms using the GRASShopper solver. We have applied our approach to a range of concurrent algorithms, including Rust’s atomic reference counter, the Linux ticketed lock, the CLH queue-lock, and a fine-grained list algorithm.},
url = {http://approjects.co.za/?big=en-us/research/publication/starling-lightweight-concurrency-verification-with-views/},
pages = {544-569},
}