Rely-guarantee bound analysis of parameterized concurrent shared-memory programs

Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3):507–534

Abdulla PA, Haziza F, Holík L, Jonsson B, Rezine A (2013) An integrated specification and verification technique for highly concurrent data structures. In: TACAS, Lecture Notes in Computer Science, vol. 7795, pp. 324–338. Springer

Albert E, Arenas P, Genaim S, Gómez-Zamalloa M, Puebla G (2012) Automatic inference of resource consumption bounds. In: LPAR, Lecture Notes in Computer Science, vol. 7180, pp. 1–11. Springer

Albert E, Arenas P, Genaim S, Puebla G (2011) Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2):161–203

Albert E, Flores-Montoya A, Genaim S, Martin-Martin E (2017) Rely-guarantee termination and cost analyses of loops with concurrent interleavings. J. Autom. Reason. 59(1):47–85

Alias C, Darte A, Feautrier P, Gonnord L (2010) Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: SAS, Lecture Notes in Computer Science, vol. 6337, pp. 117–133. Springer

Berdine J, Lev-Ami T, Manevich R, Ramalingam G, Sagiv S (2008) Thread quantification for concurrent shape analysis. In: CAV, Lecture Notes in Computer Science, vol. 5123, pp. 399–413. Springer

Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T (2011) Programs with lists are counter automata. Formal Methods Syst. Des. 38(2):158–192

Brockschmidt M, Emmes F, Falke S, Fuhs C, Giesl J (2016) Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4):13:1-13:50

Calcagno C, Distefano D, O’Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289–300. ACM

Calcagno C, Parkinson MJ, Vafeiadis V (2007) Modular safety checking for fine-grained concurrency. In: SAS,Lecture Notes in Computer Science, vol. 4634, pp. 233–248. Springer

Carbonneaux Q, Hoffmann J, Reps TW, Shao Z (2017) Automated resource analysis with coq proof objects. In: CAV (2), Lecture Notes in Computer Science, vol. 10427, pp. 64–85. Springer

Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V (2015) Aspect-oriented linearizability proofs. Logical Methods Comput Sci 11(1)

Coachman. https://github.com/thpani/coachman (2019)

Cook B, Podelski A, Rybalchenko A (2007) Proving thread termination. In: PLDI, pp. 320–330. ACM

Doherty S, Groves L, Luchangco V, Moir M (2004) Formal verification of a practical lock-free queue algorithm. In: FORTE, Lecture Notes in Computer Science, vol. 3235, pp. 97–114. Springer

Fiedor T, Holík L, Rogalewicz A, Sinn M, Vojnar T, Zuleger F (2018) From shapes to amortized complexity. In: VMCAI, Lecture Notes in Computer Science, vol. 10747, pp. 205–225. Springer

Flanagan C, Freund SN, Qadeer S (2002) Thread-modular verification for shared-memory programs. In: ESOP, Lecture Notes in Computer Science, vol. 2305, pp. 262–277. Springer

Flanagan C, Qadeer S (2003) Thread-modular model checking. In: SPIN, Lecture Notes in Computer Science, vol. 2648, pp. 213–224. Springer

Flores-Montoya A, Hähnle R (2014) Resource analysis of complex programs with cost equations. In: APLAS, Lecture Notes in Computer Science, vol. 8858, pp. 275–295. Springer

Gotsman A, Berdine J, Cook B, Sagiv M (2007) Thread-modular shape analysis. In: PLDI, pp. 266–277. ACM

Gotsman A, Cook B, Parkinson MJ, Vafeiadis V (2009) Proving that non-blocking algorithms don’t block. In: POPL, pp. 16–28. ACM

Gulwani S, Zuleger F (2010) The reachability-bound problem. In: PLDI, pp. 292–304. ACM

Hendler D, Shavit N, Yerushalmi L (2004) A scalable lock-free stack algorithm. In: SPAA, pp. 206–215. ACM

Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, USA

Holík L, Meyer R, Vojnar T, Wolff S (2017) Effect summaries for thread-modular analysis - sound analysis despite an unsound heuristic. In: SAS, Lecture Notes in Computer Science, vol. 10422, pp. 169–191. Springer

Jia X, Li W, Vafeiadis V (2015) Proving lock-freedom easily and automatically. In: CPP, pp. 119–127. ACM

Jones CB (1983) Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332. North-Holland/IFIP

Malkis A, Podelski A, Rybalchenko A (2006) Thread-modular verification is cartesian abstract interpretation. In: ICTAC, Lecture Notes in Computer Science, vol. 4281, pp. 183–197. Springer

McMillan KL (1999) Circular compositional reasoning about liveness. In: CHARME, Lecture Notes in Computer Science, vol. 1703, pp. 342–345. Springer

Michael MM, Scott ML (1996) Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267–275. ACM

Miné A (2011) Static analysis of run-time errors in embedded critical parallel C programs. In: ESOP, Lecture Notes in Computer Science, vol. 6602, pp. 398–418. Springer

Pani T, Weissenbacher G, Zuleger F (2018) Rely-guarantee reasoning for automated bound analysis of lock-free algorithms. In: FMCAD, pp. 1–9. IEEE

Petrank E, Musuvathi M, Steensgaard B (2009) Progress guarantee for parallel programs via bounded lock-freedom. In: PLDI, pp. 144–154. ACM

Reynolds JC (2002) Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society

Sinn M, Zuleger F, Veith H (2017) Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason 59(1):3–45

Ströder T, Giesl J, Brockschmidt M, Frohn F, Fuhs C, Hensel J, Schneider-Kamp P, Aschermann C (2017) Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason 58(1):33–65

Treiber RK (1986) Systems programming: Coping with parallelism. Tech. Rep. RJ 5118, IBM Almaden Research Center

Vafeiadis V (2009) Shape-value abstraction for verifying linearizability. In: VMCAI, Lecture Notes in Computer Science, vol. 5403, pp. 335–348. Springer

Vafeiadis V (2010) Automatically proving linearizability. In: CAV, Lecture Notes in Computer Science, vol. 6174, pp. 450–464. Springer

Vafeiadis V (2010) Rgsep action inference. In: VMCAI, Lecture Notes in Computer Science, vol. 5944, pp. 345–361. Springer

Xu Q, de Roever WP, He J (1997) The rely-guarantee method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2):149–174