25 papers:
ICALP-v2-2015-BouajjaniEEH #on the #reachability- On Reducing Linearizability to State Reachability (AB, ME, CE, JH), pp. 95–107.
SOSP-2015-LeePKMO #implementation #latency #scalability- Implementing linearizability at large scale and low latency (CL, SJP, AK, SM, JKO), pp. 71–86.
CAV-2015-Leslie-HurdCF #verification- Verifying Linearizability of Intel® Software Guard Extensions (RLH, DC, MF), pp. 144–160.
- CAV-2015-ZhuPJ #named #proving #smt
- Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.
ESOP-2014-ZomerGRS #encapsulation- Checking Linearizability of Encapsulated Extended Operations (OZ, GGG, GR, MS), pp. 311–330.
- ICALP-v2-2014-JagadeesanR #consistency
- Between Linearizability and Quiescent Consistency — Quantitative Quiescent Consistency (RJ, JR), pp. 220–231.
FM-2014-DerrickDSTTW #consistency #verification- Quiescent Consistency: Defining and Verifying Relaxed Linearizability (JD, BD, GS, BT, OT, HW), pp. 200–214.
IFM-2014-DerrickSD #architecture #verification- Verifying Linearizability on TSO Architectures (JD, GS, BD), pp. 341–356.
- IFM-2014-TofanSR #composition #multi #proving
- A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset (BT, GS, WR), pp. 357–372.
OOPSLA-2014-LiuTZ #named- Flint: fixing linearizability violations (PL, OT, XZ), pp. 543–560.
ASE-2013-ZhangCW #concurrent #data type #named #runtime- Round-up: Runtime checking quasi linearizability of concurrent data structures (LZ, AC, CW), pp. 4–14.
PLDI-2013-LiangF #composition #verification- Modular verification of linearizability with non-fixed linearization points (HL, XF), pp. 459–470.
- CAV-2013-DragoiGH #automation #concurrent #proving
- Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates (CD, AG, TAH), pp. 174–190.
- PLDI-2012-GuerraouiKL
- Speculative linearizability (RG, VK, GL), pp. 55–66.
STOC-2011-GolabHW #distributed #implementation #random- Linearizable implementations do not suffice for randomized distributed computation (WMG, LH, PW), pp. 373–382.
ICSE-2011-Zhang11a #automation #scalability- Scalable automatic linearizability checking (SJZ), pp. 1185–1187.
TACAS-2010-ElmasQSST #abstraction #proving #reduction- Simplifying Linearizability Proofs with Reduction and Abstraction (TE, SQ, AS, OS, ST), pp. 296–311.
- PLDI-2010-BurckhardtDMT #automation #named
- Line-up: a complete and automatic linearizability checker (SB, CD, MM, RT), pp. 330–340.
- CAV-2010-CernyRZCA #concurrent #implementation #model checking
- Model Checking of Linearizability of Concurrent List Implementations (PC, AR, DZ, SC, RA), pp. 465–479.
- CAV-2010-Vafeiadis #automation #proving
- Automatically Proving Linearizability (VV), pp. 450–464.
- FM-2009-LiuCLS #model checking #refinement
- Model Checking Linearizability via Refinement (YL, WC, YAL, JS), pp. 321–337.
VMCAI-2009-Vafeiadis #abstraction #verification- Shape-Value Abstraction for Verifying Linearizability (VV), pp. 335–348.
- PLDI-2008-VechevY #concurrent #fine-grained
- Deriving linearizable fine-grained concurrent objects (MTV, EY), pp. 125–135.
- IFM-2007-DerrickSW #proving #refinement
- Proving Linearizability Via Non-atomic Refinement (JD, GS, HW), pp. 195–214.
- CAV-2007-AmitRRSY #abstraction #comparison #verification
- Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.
