05 Nov 20

This article illustrates how to use TLA+ to formally verify (and find bugs) glibc’s pthread_cond_signal implementation.

by mlb

30 May 20

A git repository that serves as a tutorial for analyzing a blocking queue implementation using TLA+, each git commit introduces a new concept.

by mlb