log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
Starling: Simpler proofs of concurrent algorithms
Monday, October 17, 2016, 11:00 am-12:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

Logics derived from separation logic have made it feasible to reason about the most complex concurrent algorithms. However, these modern logics are enormously complex, and many lack automated tool support. 

We propose an antidote in Starling, a prototype tool for automated verification of concurrent algorithms. Starling takes a proof outline written in an intuitive predicate-based style, and converts it into proof obligations that can be discharged by Z3 or inferred by a Horn clause solver. 

Starling's underlying theory is derived from the Views framework (and ultimately from separation logic) which means it can be applied to many kinds of reasoning system. Starling can automatically challenging concurrent algorithms including the ticketed lock, atomic reference counter, reader-writer lock, and others. 

Starling is hosted on github: http://github.com/septract/starling-tool

Bio

Mike Dodds is an anniversary lecturer in the Department of Computer Science at the University of York. He is also a Royal Society industry fellow with Microsoft Research.

Mike's research is about using rigorous mathematics to solve tricky engineering problems. At the moment, he's mostly interested building and verifying multicore data-structures.

This talk is organized by Mike Hicks