Diaframe: automated verification of fine-grained concurrent programs in Iris
Ike Mulder, Robbert Krebbers, Herman Geuvers · 2022
Fine-grained concurrent programs are difficult to get right, yet play an important role in modern-day computers. We want to prove strong specifications of such programs, with minimal user effort, in a trustworthy way. In this paper, we present Diaframe—an automated and foundational verification tool for fine-grained concurrent programs.