Diaframe: automated verification of fine-grained concurrent programs in Iris
Ike Mulder, Robbert Krebbers, Herman Geuvers
Abstract
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.
Topics & Concepts
Computer scienceTrustworthinessProgramming languageIRIS (biosensor)Software engineeringComputer securityBiometricsSecurity and Verification in ComputingParallel Computing and Optimization TechniquesDistributed systems and fault tolerance