Exporters From Japan
 
Wholesale exporters from Japan   Company Established 1983
CARVIEW
MOTORHOMES
Select Language

News

April 10, 2024.
Our paper "mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic" has been conditionally accepted to the CAV 2024 tools track.

March 18, 2022.
Starting next fall I will continue teaching at UW under the new title of Assistant Teaching Professor!

November 15, 2021.
I am on the academic job market for teaching-track positions this year. I am especially interested in positions at large public universities with a commitment to serving a diverse student population. If you are hiring this year, please feel free to reach out to me.

You can also look at my generic cover letter, CV, teaching statement, and diversity statement. All my materials are also available as a single PDF.


About Me

I am assistant teaching professor of computer science at the University of Washington.

This is my academic homepage. I got my PhD at the University of Washington, where I was advised by Zach Tatlock in the PLSE group. My research interests are in programming languages, systems, and formal methods. My thesis work was on compositional techniques for verifying distributed systems implementations. I generally enjoy working with proof assistants and SMT solvers on applications to all kinds of concurrent programming. I also dabble in floating point, compilers, 3D printing, and database.

Before grad school, I did my undergraduate at Williams College, graduating in 2013, where I worked with Steve Freund on dynamic race detection. Since then Steve and I have continued to collaborate, including on an "our powers combined" paper on verified dynamic race detection with Cormac Flanagan.

Outside computer science, I enjoy good coffee, choral music, distance running, and small planes. I do not enjoy cars of any size.

I sing baritone in the St. Mark's Cathedral Choir, Evensong Choir, and Compline Choir. The Compline Choir performs each Sunday night at 9:30pm at St. Mark's. The Compline service a 30 minute chanted/sung service that tends to draw hundreds of people every week and thousands via a live radio broadcast and the podcast. It's a classic Seattle experience. You should check it out! You can listen live on King FM or get the podcast.

I occasionally play handbells.

Finally, I like to ride my bike (a Trek 520): in 2009 I biked the TransAm (east to west). I'm always thinking about my next tour.


Publications DBLP Google Scholar

  • mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic.
    James R. Wilcox, Yotam M. Y. Feldman, Oded Padon, and Sharon Shoham.
    CAV 2024. Springer. Local copy. Code.
  • Armada: Automated Verification of Concurrent Code with Sound Semantic Extensibility.
    Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Haojun Ma, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao.
    TOPLAS vol. 44 no. 2. May 2022. ACM DL. Local copy.
  • Property-Directed Reachability as Abstract Interpretation in the Monotone Theory.
    Yotam M. Y. Feldman, Sharon Shoham, Mooly Sagiv, and James R. Wilcox.
    POPL 2022. arXiv Copy.
  • Induction Duality: Primal-Dual Search for Invariants.
    Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken.
    POPL 2022. Local Copy.
  • Compositional and Automated Verification of Distributed Systems.
    James R. Wilcox.
    PhD thesis. Local Copy.
  • Learning the Boundary of Inductive Invariants.
    Yotam M. Y. Feldman, Sharon Shoham, Mooly Sagiv, and James R. Wilcox.
    POPL 2021. arXiv Copy. Local Copy. ACM DL.
  • Armada: Low-Effort Verification of High-Performance Concurrent Programs.
    Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao.
    PLDI 2020. Distinguished Paper. Local Copy. ACM DL.
  • Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations.
    Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock.
    PLDI 2020. Local Copy. ACM DL.
  • Inferring Inductive Invariants from Phase Structures.
    Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, and Mooly Sagiv.
    CAV 2019. Local Copy. Springer.
  • Functional Programming for Compiling and Decompiling Computer-Aided Design.
    Chandrakana Nandi, James R. Wilcox, Pavel Panchekha, Taylor Blau, Dan Grossman, and Zachary Tatlock.
    ICFP 2018. Local Copy. ACM DL.
  • Modularity for Decidability of Deductive Verification with Applications to Distributed Systems.
    Marcelo Taube, Giuliano Losa, Kenneth McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos.
    PLDI 2018. Local Copy. ACM DL. Source Code.
  • VerifiedFT: A Verified, High-Performance Dynamic Race Detector.
    James R. Wilcox, Cormac Flanagan, and Stephen N. Freund.
    PPoPP 2018. Local Copy. ACM DL.
  • Highlights in Systems Verification.
    James R. Wilcox.
    CACM February 2018. ACM DL.
  • Programming and Proving with Distributed Protocols.
    Ilya Sergey, James R. Wilcox, and Zachary Tatlock.
    POPL 2018. Local Copy. ACM DL. Code. Slides (Keynote). Slides (PDF).
  • Œuf: Minimizing the Coq Extraction TCB.
    Eric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, and Dan Grossman.
    CPP 2018. Local Copy. ACM DL.
  • Programming Language Abstractions for Modularly Verified Distributed Systems.
    James R. Wilcox, Ilya Sergey, and Zachary Tatlock.
    SNAPL 2017. Local Copy. Publisher Copy. Slides (Keynote). Slides (PDF).
  • Verification of Implementations of Distributed Systems Under Churn.
    Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, and Karl Palmskog.
    CoqPL 2017. Local Copy. Publisher Copy.
  • Planning for Change in a Formal Verification of the Raft Consensus Protocol.
    Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson.
    CPP 2016. Local Copy. ACM DL.
  • Sets Characterized by Missing Sums and Differences in Dilating Polytopes.
    Thao Do, Archit Kulkarni, Steven J. Miller, David Moon, Jake Wellens, and James Wilcox.
    Journal of Number Theory, December 2015. arXiv draft. Publisher copy.
  • Array Shadow State Compression for Precise Dynamic Race Detection.
    James R. Wilcox, Parker Finch, Cormac Flanagan, and Stephen N. Freund.
    ASE 2015. Local Copy. Extended Tech Report.
  • Verdi: A Framework for Formally Verifying Distributed System Implementations.
    James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson.
    PLDI 2015. Local Copy. ACM DL.
  • Automatically Improving Accuracy for Floating Point Expressions.
    Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock.
    PLDI 2015. Distinguished Paper. Local Copy. ACM DL.
  • ShrinkWrap: Efficient Dynamic Race Detection for Array-Intensive Programs.
    James Wilcox. Stephen N. Freund, Advisor.
    Williams College Undergraduate Honors Thesis, 2013. Local Copy.
  • Information-centric networking: Seeing the forest for the trees.
    Ali Ghodsi, Scott Shenker, Teemu Koponen, Ankit Singla, Barath Raghavan, and James Wilcox.
    HotNets 2011. Local Copy. ACM DL.
  • Intelligent design enables architectural evolution.
    Ali Ghodsi, Scott Shenker, Teemu Koponen, Ankit Singla, Barath Raghavan, and James Wilcox.
    HotNets 2011. Local Copy. ACM DL.

Blog

Subscribe [Valid RSS]

April 29, 2022. (Last updated: October 2024)
Teaching Principles
This living document collects James's Teaching Principles™.

February 21, 2017.
Exercises on Generalizing the Induction Hypothesis.
This post collects several Coq exercises on generalizing the induction hypothesis.

January 9, 2017.
A Port of the Proof of Peterson's Algorithm to Dafny.
This code-only post is a port of the proof of Peterson's Algorithm to Dafny. It also serves as a good example of how to reason about concurrent systems in Dafny, essentially by writing a thread scheduler.

April 24, 2016.
How to build a simple system in Verdi.
In this long-awaited post, we'll show how to implement and verify a simple distributed system using network semantics.

May 8, 2015
A Proof of Peterson's Algorithm.
In this post, we take a break from distributed systems to look at shared memory systems. As a case study, we give a proof that Peterson's algorithm provides mutual exclusion.

April 16, 2015
Network Semantics for Verifying Distributed Systems.
This is the first post in a series on Verdi. In this post, we'll get our feet wet by defining a formal model of how distributed systems execute on the network.

October 20, 2014
Reasoning about Cardinalities of Sums and Products.
In this short, code-heavy post, we extend some of the work from a previous post to reason about the cardinalities of sums and products.

September 14, 2014
Dependent Case Analysis in Coq without Axioms.
This post shows how to get around the limitations of the destruct tactic when doing case analysis on dependent types, without resorting to the dependent destruction tactic, which relies on additional axioms.

September 4, 2014
"run" + "time" = ???.
This brief post records Mike's description of the three ways of combining the words "run" and "time" in computer science writing.

June 12, 2014
"More Sums than Differences" Sets, Part 2: Counting MSTD Sets.
This is the (much delayed) second post in a series on More Sums than Difference Sets. In this post, we'll take a first crack at the question, "How many MSTD sets are there?" To do so, we'll write a straightforward C program that counts MSTD sets. Then we'll run it to count MSTD sets and benchmark its performance.

April 10, 2014
Tail Recursion Modulo cons.
Tail recursion has come up in a few conversations this week. This post explores a generalization of tail call optimization that I wasn't aware of until Doug described it to me.

March 3, 2014
"More Sums than Differences" Sets, Part 1: A puzzle.
This is the first post in a series on "More Sums than Differences" Sets. In this post, we'll get our terminology straight and ask a lot of questions.

December 31, 2013
Easy access to the off-campus proxy.
I use the UW proxy to access the ACM digital library from off campus, but it's annoying to type the proxy URL every time I click a link to a new paper. Here are two ways to make life easier.



Teaching

At UW:

Service

  • PLDI 2023 PC member
  • POPL 2022 PC member
  • OSDI 2021 ERC member
  • ASPLOS 2021 ERC member
  • VMCAI 2021 PC member
  • OOPSLA 2020 external reviewer
  • PLDI 2019 external reviewer
  • POPL 2019 external reviewer
  • OOPSLA 2018 external reviewer
  • POPL 2017 external reviewer
© James R. Wilcox. Last updated: October 2024
 
Original Source | Taken Source