Anil Madhavapeddy

On the challenge of delivering high-performance, dependable, model-checked internet servers / Jun 2005

Paper on temporal automata for protocol implementations at HotDep 2005. This work, done with Dave Scott, explored the challenge of building internet servers that are simultaneously high-performance, dependable, and formally verified through model checking. We investigated how to use temporal automata to specify and verify protocol implementations without sacrificing the performance needed for production systems. The key insight was finding ways to make formal verification practical for real-world network services.