!(Screen Shot 2021-04-04 at 11.31.59 AM.png)
Last week in the Distributed Systems Reading Group we read Aragog: Scalable Runtime Verification of Shardable Networked Systems. The paper describes an intriguing system from Microsoft Research and U Penn; it can analyze huge numbers of network events and find invariant violations that indicate bugs in the protocol. The invariants are expressed in a cute regular expression language, which Aragog parses and automatically decomposes into local and global verifier state machines. (But I don’t know why it’s called “Aragog”.)
Read Aleksey Charapko’s summary or watch my presentation.