Linked Presentation: Automated Verification of Customizable Middlebox Properties with Gravel Programmable Calendar Queues for High-speed Packet Scheduling Fine-Grained Replicated State Machines for a Cluster Storage System