A colleague told me about a multithreaded algorithm that was later reported to have a bug. I rewrote the algorithm in the ~+CAL algorithm language, ran the TLC model checker on it, and found the error. Programs are not released without being tested; why should algorithms be published without being model checked?
展开▼
