Information-centric networking: seeing the forest for the trees. - Ali Ghodsi 002; Scott Shenker; Teemu Koponen; Ankit Singla; Barath Raghavan; James Wilcox 001 (HotNets, 2011)

Intelligent design enables architectural evolution. - Ali Ghodsi 002; Scott Shenker; Teemu Koponen; Ankit Singla; Barath Raghavan; James Wilcox 001 (HotNets, 2011)

Array Shadow State Compression for Precise Dynamic Race Detection (T). - James R. Wilcox; Parker Finch; Cormac Flanagan; Stephen N. Freund (ASE, 2015)

Automatically improving accuracy for floating point expressions. - Pavel Panchekha; Alex Sanchez-Stern; James R. Wilcox; Zachary Tatlock (PLDI, 2015)

Verdi: a framework for implementing and formally verifying distributed systems. - James R. Wilcox; Doug Woos; Pavel Panchekha; Zachary Tatlock; Xi Wang 005; Michael D. Ernst; Thomas E. Anderson (PLDI, 2015)

Planning for change in a formal verification of the raft consensus protocol. - Doug Woos; James R. Wilcox; Steve Anton; Zachary Tatlock; Michael D. Ernst; Thomas E. Anderson (CPP, 2016)

Programming Language Abstractions for Modularly Verified Distributed Systems. - James R. Wilcox; Ilya Sergey; Zachary Tatlock (SNAPL, 2017)

Private Online Communication; Highlights in Systems Verification. - Albert Kwon; James Wilcox 001 (ACM Queue, 2017)

Œuf: minimizing the Coq extraction TCB. - Eric Mullen; Stuart Pernsteiner; James R. Wilcox; Zachary Tatlock; Dan Grossman (CPP, 2018)

Modularity for decidability of deductive verification with applications to distributed systems. - Marcelo Taube; Giuliano Losa; Kenneth L. McMillan; Oded Padon; Mooly Sagiv; Sharon Shoham; James R. Wilcox; Doug Woos (PLDI, 2018)

VerifiedFT: a verified, high-performance precise dynamic race detector. - James R. Wilcox; Cormac Flanagan; Stephen N. Freund (PPoPP, 2018)

Research for practice: private online communication; highlights in systems verification. - Albert Kwon; James R. Wilcox; Peter Bailis (Commun. ACM, 2018)

Functional programming for compiling and decompiling computer-aided design. - Chandrakana Nandi; James R. Wilcox; Pavel Panchekha; Taylor Blau; Dan Grossman; Zachary Tatlock (Proc. ACM Program. Lang., 2018)

Programming and proving with distributed protocols. - Ilya Sergey; James R. Wilcox; Zachary Tatlock (Proc. ACM Program. Lang., 2018)

Inferring Inductive Invariants from Phase Structures. - Yotam M. Y. Feldman; James R. Wilcox; Sharon Shoham; Mooly Sagiv (CAV (2), 2019)

Using E-Graphs for CAD Parameter Inference. - Chandrakana Nandi; Adam Anderson 004; Max Willsey; James R. Wilcox; Eva Darulova; Dan Grossman; Zachary Tatlock (CoRR, 2019)

Armada: low-effort verification of high-performance concurrent programs. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (PLDI, 2020)

Synthesizing structured CAD models with equality saturation and inverse transformations. - Chandrakana Nandi; Max Willsey; Adam Anderson 004; James R. Wilcox; Eva Darulova; Dan Grossman; Zachary Tatlock (PLDI, 2020)

Learning the boundary of inductive invariants. - Yotam M. Y. Feldman; Mooly Sagiv; Sharon Shoham; James R. Wilcox (Proc. ACM Program. Lang., 2021)

Compositional and Automated Verification of Distributed Systems. - James R. Wilcox (2021)

Property-directed reachability as abstract interpretation in the monotone theory. - Yotam M. Y. Feldman; Mooly Sagiv; Sharon Shoham; James R. Wilcox (Proc. ACM Program. Lang., 2022)

Induction duality: primal-dual search for invariants. - Oded Padon; James R. Wilcox; Jason R. Koenig; Kenneth L. McMillan; Alex Aiken (Proc. ACM Program. Lang., 2022)

Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility. - Jacob R. Lorch; Yixuan Chen 002; Manos Kapritsos; Haojun Ma; Bryan Parno; Shaz Qadeer; Upamanyu Sharma; James R. Wilcox; Xueyuan Zhao (ACM Trans. Program. Lang. Syst., 2022)

mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic. - James R. Wilcox; Yotam M. Y. Feldman; Oded Padon; Sharon Shoham (CAV (2), 2024)