Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources

Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco

Recent approaches to verifying programs in separation logics for concurrency have used state transition systems (STSs) to specify the atomic operations of programs. A key challenge…