Publications

• Kuan-Yen Chou. Scalable Verification for Complex Networks. In PhD dissertation, University of Illinois Urbana-Champaign, November 2024.

  [paper]
• Kuan-Yen Chou, Santhosh Prabhu, Giri Subramanian, Wenxuan Zhou, Aanand Nayyar, Brighten Godfrey, Matthew Caesar. Fine-grained Distributed Data Plane Verification with Intent-based Slicing. In arXiv, May 2024.

  [paper]
• Santhosh Prabhu, Kuan-Yen Chou, Aanand Nayyar, Giri Prashanth Subramanian, Wenxuan Zhou, Philip Brighten Godfrey. Handling device configuration changes in distributed network verification application. In US Patent 2024/0086221 A1, March 2024.

  [paper]
• Santhosh Prabhu, Kuan-Yen Chou, Aanand Nayyar, Giri Prashanth Subramanian, Wenxuan Zhou, Philip Brighten Godfrey. Evaluation of network correctness requirement. In US Patent 2024/0089257 A1, March 2024.

  [paper]
• Santhosh Prabhu, Kuan-Yen Chou, Aanand Nayyar, Giri Prashanth Subramanian, Wenxuan Zhou, Philip Brighten Godfrey. Distributed network verification. In US Patent 2024/0089184 A1, March 2024.

  [paper]
• Bingzhe Liu, Kuan-Yen Chou, Pramod Jamkhedkar, Bilal Anwer, Rakesh K Sinha, Kostas Oikonomou, Matthew Caesar, P. Brighten Godfrey. Practical Automation for Management Planes of Service Provider Infrastructure. In FlexNets, August 2021.

  [paper]
• Santhosh Prabhu, Kuan-Yen Chou, Ali Kheradmand, P. Brighten Godfrey, Matthew Caesar. Plankton: Scalable network configuration verification through model checking. In USENIX NSDI, February 2020.

  [paper] [video]
• Sayed Hadi Hashemi, Paul Rausch, Benjamin Rabe, Kuan-Yen Chou, Simeng Liu, Volodymyr V. Kindratenko, Roy H. Campbell. tensorflow-tracing: A Performance Tuning Framework for Production. In USENIX OpML, May 2019.

  [paper] [slides] [code]
• Kuan-Yen Chou, Chin-Fan Chiang, Ching-Hsiang Hsu, Zheng-Yu Chen, Jin-Cheng Zhu. Implementation of Containerized TensorFlow in Heterogeneous CPU/GPU Clusters. In Taiwan Academic Network Conference, October 2017.

  [paper]

Systems

• Scylla

  A distributed data plane verifier that slices the network model at intent granularity and spreads the slices across a compute cluster, so verification cost scales with the intents being checked rather than with network size.

  • Fine-grained Distributed Data Plane Verification with Intent-based Slicing (arXiv, 2024)
  • Handling device configuration changes in distributed network verification application (US Patent 2024/0086221 A1, 2024)
  • Distributed network verification (US Patent 2024/0089184 A1, 2024)
  • Evaluation of network correctness requirement (US Patent 2024/0089257 A1, 2024)

• Mimesis

  Automated extraction of formal packet-forwarding models directly from network program binaries, using full-system symbolic execution and dynamic instrumentation. Models are encoded as BDDs and work with existing verifiers; demonstrated on userspace NFs, kernel NFs, and eBPF programs.

  • Source code

• Neo

  A concolic network testing framework that combines symbolic model checking with emulation: software devices run as concrete processes while the rest of the network is explored exhaustively, covering in-network nondeterminism without hand-written models.

  • Source code

• Plankton

  A network configuration verifier that combines equivalence partitioning of packet header space with explicit-state model checking, exhaustively verifying all converged states a control plane configuration can reach, orders of magnitude faster than prior work.

  • Plankton: Scalable network configuration verification through model checking (USENIX NSDI, 2020)