Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, Benjamin Chelf · SOSP 2001

code says what it believes by repeating it. heresy counts how often a rule holds across a go codebase and flags the sites that break one kept hundreds of times. lock release and nil checks so far, run on 16 big repos.

Shuming Ma et al. · arXiv 2024

the paper shows ternary weights lose little accuracy. the kernel side is where the published work thins out, so ciot is that part: a ternary matvec on arm neon with no multiplies, checked bit for bit against a scalar reference.

Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner · Logical Methods in Computer Science, 2011

a compiler usually rewrites the program pass by pass, and every pass throws away the version before it, so the order of the passes decides what you end up with. this paper keeps every equal version at once in one graph, and picks the best one at the end. no pass order to get wrong. it is the idea under e-graphs and egg.