Date: January 30, 2026
Title: Deciding Serializability in Network Systems (TACAS 2026)
Speaker: Guy Amir, Postdoctoral Researcher, Cornell University
Abstract: We present the SER modeling language for automatically verifying serializability of transactional programs, i.e., whether every concurrent execution of the program is equivalent to some serial execution. SER programs are suitably restricted to make this problem decidable, while still allowing for an unbounded number of concurrent threads of execution, each potentially running for an unbounded number of steps. We give the first automated end-to-end decision procedure that either proves serializability by producing a checkable certificate, or refutes it by producing a counterexample trace. Furthermore, we present a network-system abstraction that captures serializability through the lens of software-defined networks, and put forth various optimizations for curtailing the search space. We extensively evaluate our framework on models of real-world programs, including stateful firewalls, BGP routers, and more.
Bio: Guy Amir is a postdoctoral researcher at Cornell University working at the intersection of formal methods, concurrency, and systems. He earned his Ph.D. from the Hebrew University of Jerusalem, where he focused on the formal verification of neural networks.