A. Jesse Jiryu Davis

Category: Research

Two attempts to compare a TLA+ spec with a C++ implementation At MongoDB we tried two methods to test that a spec matches the code: one worked, one didn't. We explain our results in a VLDB 2020 paper.