1 citations · 2 across the 3 of their papers we have counts for
3 papers · 1 filter
Local Reasoning for Global Graph Properties
Siddharth Krishna, Alexander J. Summers, Thomas Wies
Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expres…
Verifying Visibility-Based Weak Consistency
Siddharth Krishna, Michael Emmi, Constantin Enea +1
Multithreaded programs generally leverage efficient and thread-safe concurrent objects like sets, key-value maps, and queues. While some concurrent-object operations are designed t…
Go with the Flow: Compositional Abstractions for Concurrent Data Structures (Extended Version)
Siddharth Krishna, Dennis Shasha, Thomas Wies
Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data struc…