---
title: "基于交互式定理证明的并发程序验证工作综述 — 王中烨 2024"
description: "This Chinese-language survey from Shanghai Jiao Tong University examines how interactive theorem provers such as Coq and Isabelle/HOL can rigorously…"
authors: ["王中烨", "吴姝姝", "曹钦翔"]
year: 2024
venue: "软件学报 (Journal of Software)"
source: "https://jos.org.cn/jos/article/abstract/7138"
doi: "10.13328/j.cnki.jos.007138"
licence: "Free access (jos.org.cn), no open licence stated — readonly; © 中国科学院软件研究所 / 软件学报"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/papers/wang-2024-interactive-theorem-proving/"
---
[Elamur Research](https://md.research.elamur.ai/) · [this page in HTML](https://research.elamur.ai/free/papers/wang-2024-interactive-theorem-proving/)

[home](https://md.research.elamur.ai/) / [papers](https://md.research.elamur.ai/free/papers/) / [2024](https://md.research.elamur.ai/free/papers/2024/page/4/) / 基于交互式定理证明的并发程序验证工作综述

# 基于交互式定理证明的并发程序验证工作综述

**Authors:** 王中烨, 吴姝姝, 曹钦翔 · **Year:** 2024 · **Venue:** 软件学报 (Journal of Software) · **Licence:** Free access (jos.org.cn), no open licence stated — readonly; © 中国科学院软件研究所 / 软件学报

**Links:** [Publisher's page](https://doi.org/10.13328/j.cnki.jos.007138) · [PDF](http://rjxb.alljournals.cn/jos/article/pdf/7138) · [DOI 10.13328/j.cnki.jos.007138](https://doi.org/10.13328/j.cnki.jos.007138)

## Summary
This Chinese-language survey from Shanghai Jiao Tong University examines how interactive theorem provers such as Coq and Isabelle/HOL can rigorously establish the correctness of concurrent software. Concurrent programs are hard to verify because thread interleavings are non-deterministic, so testing can easily miss bugs. The authors first compare this approach with model checking and SMT-backed automated proving. They then propose four dimensions for classifying verification work: the programming language, the concurrency primitives supported, the semantics and memory model, and the verification goal.

The core of the survey sets out four functional-correctness targets and explains how they relate:
- Hoare triples under a constrained concurrent context
- linearizability
- contextual refinement
- logical atomicity

It then reviews three families of program logic used to prove these targets: concurrent separation logic, rely-guarantee reasoning and relational Hoare logic. Finally, it catalogues tools and verified systems built on these logics. The paper offers a structured map of a fragmented field and helps readers choose a suitable specification and proof technique for a given concurrent system.

## Key points
- Published in 软件学报 (Journal of Software), 2024, vol. 35(9), pp. 4069–4099 (doi: 10.13328/j.cnki.jos.007138).
- The survey mainly assumes a sequentially consistent memory model and treats weak memory models (TSO, C11) only briefly.
- A running queue example (`enq`/`deq`) shows why plain Hoare triples become too weak once other threads may touch shared state. This motivates linearizability and the other general-context criteria.
- The automated proof-outline checkers covered include Starling and Caper (built on Z3), Diaframe (built on Iris) and Voila (built on Viper/TADA).
- Foundational frameworks and results discussed include VST, Iris, RustBelt, RefinedC, CSimpl, Perennial and GoJournal, as well as AtomFS and Zephyr RTOS memory management.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

Fields: [Linguistics & languages](https://md.research.elamur.ai/free/shelves/linguistics/) · [Natural language processing](https://md.research.elamur.ai/free/shelves/nlp/)

## Cite

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@article{2024,
  title = {{基于交互式定理证明的并发程序验证工作综述}},
  author = {王中烨 and 吴姝姝 and 曹钦翔},
  journal = {软件学报 (Journal of Software)},
  year = {2024},
  doi = {10.13328/j.cnki.jos.007138},
  url = {https://doi.org/10.13328/j.cnki.jos.007138}
}
```

- [← previous 可控文本生成技术研究综述](https://md.research.elamur.ai/free/papers/wang-2024-controllable-text-generation/)
- [next → 基于大语言模型的事件常识知识图谱扩展方法](https://md.research.elamur.ai/free/papers/huang-2024-method-expanding-event/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/papers/2024/page/4/)

## References

108 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Lamport L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. on Computers, 1979, C-28(9): 690–691. [doi: 10.1109/TC.1979.1675439] — [doi:10.1109/tc.1979.1675439](https://doi.org/10.1109/tc.1979.1675439) [find](https://scholar.google.com/scholar?q=Lamport+L%2E+How+to+make+a+multiprocessor+computer+that+correctly+executes+multiprocess+programs%2E+IEEE+Trans%2E+on+Computers%2C+1979%2C+C%2D28%289%29%3A+690%E2%80%93691%2E+%5Bdoi%3A+10%2E1109%2FTC%2E1979%2E1675439%5D+%E2%80%94+%5Bdoi%3A10%2E1109%2Ftc%2E1979%2E)
2. Herlihy MP, Wing JM. Linearizability: A correctness condition for concurrent objects. ACM Trans. on Programming Languages and Systems, 1990, 12(3): 463–492. [doi: 10.1145/78969.78972] — [doi:10.1145/78969.78972](https://doi.org/10.1145/78969.78972) [find](https://scholar.google.com/scholar?q=Herlihy+MP%2C+Wing+JM%2E+Linearizability%3A+A+correctness+condition+for+concurrent+objects%2E+ACM+Trans%2E+on+Programming+Languages+and+Systems%2C+1990%2C+12%283%29%3A+463%E2%80%93492%2E+%5Bdoi%3A+10%2E1145%2F78969%2E78972%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F7)
3. Bernstein PA, Hadzilacos V, Goodman N. Concurrency Control and Recovery in Database Systems. Reading: Addison-Wesley, 1987. [find](https://scholar.google.com/scholar?q=Bernstein+PA%2C+Hadzilacos+V%2C+Goodman+N%2E+Concurrency+Control+and+Recovery+in+Database+Systems%2E+Reading%3A+Addison%2DWesley%2C+1987%2E)
4. Liang HJ, Feng XY. Progress of concurrent objects. Foundations and Trends® in Programming Languages, 2020, 5(4): 282–414. [doi: 10.1561/2500000041] — [doi:10.1561/2500000041](https://doi.org/10.1561/2500000041) [find](https://scholar.google.com/scholar?q=Liang+HJ%2C+Feng+XY%2E+Progress+of+concurrent+objects%2E+Foundations+and+Trends%C2%AE+in+Programming+Languages%2C+2020%2C+5%284%29%3A+282%E2%80%93414%2E+%5Bdoi%3A+10%2E1561%2F2500000041%5D+%E2%80%94+%5Bdoi%3A10%2E1561%2F2500000041%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1561%2F2)
5. Herlihy M, Shavit N. On the nature of progress. In: Proc. of the 15th Int’l Conf. on Principles of Distributed Systems. Toulouse: Springer, 2011. 313–328. [doi: 10.1007/978-3-642-25873-2_22] — [doi:10.1007/978-3-642-25873-2_22](https://doi.org/10.1007/978-3-642-25873-2_22) [find](https://scholar.google.com/scholar?q=Herlihy+M%2C+Shavit+N%2E+On+the+nature+of+progress%2E+In%3A+Proc%2E+of+the+15th+Int%E2%80%99l+Conf%2E+on+Principles+of+Distributed+Systems%2E+Toulouse%3A+Springer%2C+2011%2E+313%E2%80%93328%2E+%5Bdoi%3A+10%2E1007%2F978%2D3%2D642%2D25873%2D2%5F22%5D+%E2%80%94+%5Bdoi%3A10)
6. Biere A. Bounded model checking. In: Biere A, Heule M, van Maaren H, Walsh T, eds. Handbook of Satisfiability. IOS Press, 2009. 457–481. [doi: 10.3233/978-1-58603-929-5-457] — [doi:10.3233/978-1-58603-929-5-457](https://doi.org/10.3233/978-1-58603-929-5-457) [find](https://scholar.google.com/scholar?q=Biere+A%2E+Bounded+model+checking%2E+In%3A+Biere+A%2C+Heule+M%2C+van+Maaren+H%2C+Walsh+T%2C+eds%2E+Handbook+of+Satisfiability%2E+IOS+Press%2C+2009%2E+457%E2%80%93481%2E+%5Bdoi%3A+10%2E3233%2F978%2D1%2D58603%2D929%2D5%2D457%5D+%E2%80%94+%5Bdoi%3A10%2E3233%2F978%2D1%2D58603)
7. Inverso O, Tomasco E, Fischer B, La Torre S, Parlato G. Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Proc. of the 26th Int’l Conf. on Computer Aided Verification. Vienna: Springer Int’l Publishing, 2014. 585–602. [doi: 10.1007/978-3-319-08867-9_39] — [doi:10.1007/978-3-319-08867-9_39](https://doi.org/10.1007/978-3-319-08867-9_39) [find](https://scholar.google.com/scholar?q=Inverso+O%2C+Tomasco+E%2C+Fischer+B%2C+La+Torre+S%2C+Parlato+G%2E+Bounded+model+checking+of+multi%2Dthreaded+C+programs+via+lazy+sequentialization%2E+In%3A+Proc%2E+of+the+26th+Int%E2%80%99l+Conf%2E+on+Computer+Aided+Verification)
8. Flanagan C, Godefroid P. Dynamic partial-order reduction for model checking software. ACM SIGPLAN Notices, 2005, 40(1): 110–121. [doi: 10.1145/1047659.1040315] — [doi:10.1145/1047659.1040315](https://doi.org/10.1145/1047659.1040315) [find](https://scholar.google.com/scholar?q=Flanagan+C%2C+Godefroid+P%2E+Dynamic+partial%2Dorder+reduction+for+model+checking+software%2E+ACM+SIGPLAN+Notices%2C+2005%2C+40%281%29%3A+110%E2%80%93121%2E+%5Bdoi%3A+10%2E1145%2F1047659%2E1040315%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F1047659%2E1040315%5D%28https%3A%2F%2F)
9. Alglave J, Kroening D, Tautschnig M. Partial orders for efficient bounded model checking of concurrent software. In: Proc. of the 25th Int’l Conf. on Computer Aided Verification. Saint Petersburg: Springer, 2013. 141–157. [doi: 10.1007/978-3-642-39799-8_9] — [doi:10.1007/978-3-642-39799-8_9](https://doi.org/10.1007/978-3-642-39799-8_9) [find](https://scholar.google.com/scholar?q=Alglave+J%2C+Kroening+D%2C+Tautschnig+M%2E+Partial+orders+for+efficient+bounded+model+checking+of+concurrent+software%2E+In%3A+Proc%2E+of+the+25th+Int%E2%80%99l+Conf%2E+on+Computer+Aided+Verification%2E+Saint+Petersburg%3A+Spr)
10. Godefroid P. Model checking for programming languages using VeriSoft. In: Proc. of the 24th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Paris: ACM, 1997. 174–186. [doi: 10.1145/263699.263717] — [doi:10.1145/263699.263717](https://doi.org/10.1145/263699.263717) [find](https://scholar.google.com/scholar?q=Godefroid+P%2E+Model+checking+for+programming+languages+using+VeriSoft%2E+In%3A+Proc%2E+of+the+24th+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Languages%2E+Paris%3A+ACM%2C+1997%2E+174%E2%80%93186%2E+%5Bdoi%3A+10%2E1145%2F26)
11. Abdulla PA, Aronis S, Atig MF, Jonsson B, Leonardsson C, Sagonas K. Stateless model checking for TSO and PSO. Acta Informatica, 2017, 54(8): 789–818. [doi: 10.1007/s00236-016-0275-0] — [doi:10.1007/s00236-016-0275-0](https://doi.org/10.1007/s00236-016-0275-0) [find](https://scholar.google.com/scholar?q=Abdulla+PA%2C+Aronis+S%2C+Atig+MF%2C+Jonsson+B%2C+Leonardsson+C%2C+Sagonas+K%2E+Stateless+model+checking+for+TSO+and+PSO%2E+Acta+Informatica%2C+2017%2C+54%288%29%3A+789%E2%80%93818%2E+%5Bdoi%3A+10%2E1007%2Fs00236%2D016%2D0275%2D0%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2Fs0)
12. Huang J. Stateless model checking concurrent programs with maximal causality reduction. ACM SIGPLAN Notices, 2015, 50(6): 165–174. [doi: 10.1145/2813885.2737975] — [doi:10.1145/2813885.2737975](https://doi.org/10.1145/2813885.2737975) [find](https://scholar.google.com/scholar?q=Huang+J%2E+Stateless+model+checking+concurrent+programs+with+maximal+causality+reduction%2E+ACM+SIGPLAN+Notices%2C+2015%2C+50%286%29%3A+165%E2%80%93174%2E+%5Bdoi%3A+10%2E1145%2F2813885%2E2737975%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F2813885%2E2737975%5D%28https%3A)
13. Kokologiannakis M, Lahav O, Sagonas K, Vafeiadis V. Effective stateless model checking for C/C++ concurrency. Proc. of the ACM on Programming Languages, 2017, 2: 17. [doi: 10.1145/3158105] — [doi:10.1145/3158105](https://doi.org/10.1145/3158105) [find](https://scholar.google.com/scholar?q=Kokologiannakis+M%2C+Lahav+O%2C+Sagonas+K%2C+Vafeiadis+V%2E+Effective+stateless+model+checking+for+C%2FC%2B%2B+concurrency%2E+Proc%2E+of+the+ACM+on+Programming+Languages%2C+2017%2C+2%3A+17%2E+%5Bdoi%3A+10%2E1145%2F3158105%5D+%E2%80%94+%5Bdoi%3A10%2E1)
14. Huet G, Kahn G, Paulin-Mohring C. The Coq proof assistant a tutorial. Technical Report, 1997, 178. [http://www.itpro.titech.ac.jp/coq.8.2/Tutorial.pdf](http://www.itpro.titech.ac.jp/coq.8.2/Tutorial.pdf) [↗](http://www.itpro.titech.ac.jp/coq.8.2/Tutorial.pdf)
15. Nipkow T, Wenzel M, Paulson LC. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Berlin: Springer, 2002. [doi: 10.1007/3-540-45949-9] — [doi:10.1007/3-540-45949-9](https://doi.org/10.1007/3-540-45949-9) [find](https://scholar.google.com/scholar?q=Nipkow+T%2C+Wenzel+M%2C+Paulson+LC%2E+Isabelle%2FHOL%3A+A+Proof+Assistant+for+Higher%2Dorder+Logic%2E+Berlin%3A+Springer%2C+2002%2E+%5Bdoi%3A+10%2E1007%2F3%2D540%2D45949%2D9%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2F3%2D540%2D45949%2D9%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2F3%2D540)
16. Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576–580. [doi: 10.1145/363235.363259] — [doi:10.1145/363235.363259](https://doi.org/10.1145/363235.363259) [find](https://scholar.google.com/scholar?q=Hoare+CAR%2E+An+axiomatic+basis+for+computer+programming%2E+Communications+of+the+ACM%2C+1969%2C+12%2810%29%3A+576%E2%80%93580%2E+%5Bdoi%3A+10%2E1145%2F363235%2E363259%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F363235%2E363259%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1145%2F363235%2E3632)
17. Stark EW. A proof technique for rely/guarantee properties. In: Proc. of the 5th Conf. on Foundations of Software Technology and Theoretical Computer Science. New Delhi: Springer, 1985. 369–391. [doi: 10.1007/3-540-16042-6_21] — [doi:10.1007/3-540-16042-6_21](https://doi.org/10.1007/3-540-16042-6_21) [find](https://scholar.google.com/scholar?q=Stark+EW%2E+A+proof+technique+for+rely%2Fguarantee+properties%2E+In%3A+Proc%2E+of+the+5th+Conf%2E+on+Foundations+of+Software+Technology+and+Theoretical+Computer+Science%2E+New+Delhi%3A+Springer%2C+1985%2E+369%E2%80%93391%2E+%5Bdoi%3A+)
18. Jones CB. Specification and design of (parallel) programs. In: Proc. of the 9th IFIP World Computer Congress (Information Processing 83). Paris: North-Holland/IFIP, 1983. 321–332. [find](https://scholar.google.com/scholar?q=Jones+CB%2E+Specification+and+design+of+%28parallel%29+programs%2E+In%3A+Proc%2E+of+the+9th+IFIP+World+Computer+Congress+%28Information+Processing+83%29%2E+Paris%3A+North%2DHolland%2FIFIP%2C+1983%2E+321%E2%80%93332%2E)
19. O'Hearn PW. Resources, concurrency, and local reasoning. Theoretical Computer Science, 2007, 375(1–3): 271–307. [doi: 10.1016/j.tcs.2006.12.035] — [doi:10.1016/j.tcs.2006.12.035](https://doi.org/10.1016/j.tcs.2006.12.035) [find](https://scholar.google.com/scholar?q=O%27Hearn+PW%2E+Resources%2C+concurrency%2C+and+local+reasoning%2E+Theoretical+Computer+Science%2C+2007%2C+375%281%E2%80%933%29%3A+271%E2%80%93307%2E+%5Bdoi%3A+10%2E1016%2Fj%2Etcs%2E2006%2E12%2E035%5D+%E2%80%94+%5Bdoi%3A10%2E1016%2Fj%2Etcs%2E2006%2E12%2E035%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E10)
20. Tait WW. Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic, 1967, 32(2): 198–212. [doi: 10.2307/2271658] — [doi:10.2307/2271658](https://doi.org/10.2307/2271658) [find](https://scholar.google.com/scholar?q=Tait+WW%2E+Intensional+interpretations+of+functionals+of+finite+type+I%2E+The+Journal+of+Symbolic+Logic%2C+1967%2C+32%282%29%3A+198%E2%80%93212%2E+%5Bdoi%3A+10%2E2307%2F2271658%5D+%E2%80%94+%5Bdoi%3A10%2E2307%2F2271658%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E2307%2F227165)
21. Windsor M, Dodds M, Simner B, Parkinson MJ. Starling: Lightweight concurrency verification with views. In: Proc. of the 29th Int’l Conf. on Computer Aided Verification. Heidelberg: Springer Int’l Publishing, 2017. 544–569. [doi: 10.1007/978-3-319-63387-9_27] — [doi:10.1007/978-3-319-63387-9_27](https://doi.org/10.1007/978-3-319-63387-9_27) [find](https://scholar.google.com/scholar?q=Windsor+M%2C+Dodds+M%2C+Simner+B%2C+Parkinson+MJ%2E+Starling%3A+Lightweight+concurrency+verification+with+views%2E+In%3A+Proc%2E+of+the+29th+Int%E2%80%99l+Conf%2E+on+Computer+Aided+Verification%2E+Heidelberg%3A+Springer+Int%E2%80%99l+Publ)
22. Dinsdale-Young T, da Rocha Pinto P, Andersen KJ, Birkedal L. Caper: Automatic verification for fine-grained concurrency. In: Proc. of the 26th European Symp. on Programming: Programming Languages and Systems. Uppsala: Springer, 2017. 420–447. [doi: 10.1007/978-3-662-54434-1_16] — [doi:10.1007/978-3-662-54434-1_16](https://doi.org/10.1007/978-3-662-54434-1_16) [find](https://scholar.google.com/scholar?q=Dinsdale%2DYoung+T%2C+da+Rocha+Pinto+P%2C+Andersen+KJ%2C+Birkedal+L%2E+Caper%3A+Automatic+verification+for+fine%2Dgrained+concurrency%2E+In%3A+Proc%2E+of+the+26th+European+Symp%2E+on+Programming%3A+Programming+Languages+and+)
23. De Moura L, Bjørner N. Z3: An efficient SMT solver. In: Proc. of the 14th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Budapest: Springer, 2008. 337–340. [doi: 10.1007/978-3-540-78800-3_24] [find](https://scholar.google.com/scholar?q=De+Moura+L%2C+Bj%C3%B8rner+N%2E+Z3%3A+An+efficient+SMT+solver%2E+In%3A+Proc%2E+of+the+14th+Int%E2%80%99l+Conf%2E+on+Tools+and+Algorithms+for+the+Construction+and+Analysis+of+Systems%2E+Budapest%3A+Springer%2C+2008%2E+337%E2%80%93340%2E+%5Bdoi%3A+10%2E)
24. Dinsdale-Young T, Birkedal L, Gardner P, Parkinson M, Yang H. Views: Compositional reasoning for concurrent programs. In: Proc. of the 40th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Rome: ACM, 2013. 287–300. [doi: 10.1145/2429069.2429104] — [doi:10.1145/2429069.2429104](https://doi.org/10.1145/2429069.2429104) [find](https://scholar.google.com/scholar?q=Dinsdale%2DYoung+T%2C+Birkedal+L%2C+Gardner+P%2C+Parkinson+M%2C+Yang+H%2E+Views%3A+Compositional+reasoning+for+concurrent+programs%2E+In%3A+Proc%2E+of+the+40th+Annual+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming)
25. Dinsdale-Young T, Dodds M, Gardner P, Parkinson MJ, Vafeiadis V. Concurrent abstract predicates. In: Proc. of the 24th European Conf. on ECOOP 2010—Object-oriented Programming. Maribor: Springer, 2010. 504–528. [doi: 10.1007/978-3-642-14107-2_24] — [doi:10.1007/978-3-642-14107-2_24](https://doi.org/10.1007/978-3-642-14107-2_24) [find](https://scholar.google.com/scholar?q=Dinsdale%2DYoung+T%2C+Dodds+M%2C+Gardner+P%2C+Parkinson+MJ%2C+Vafeiadis+V%2E+Concurrent+abstract+predicates%2E+In%3A+Proc%2E+of+the+24th+European+Conf%2E+on+ECOOP+2010%E2%80%94Object%2Doriented+Programming%2E+Maribor%3A+Springer%2C+2010)
26. Mulder I, Krebbers R, Geuvers H. Diaframe: Automated verification of fine-grained concurrent programs in Iris. In: Proc. of the 43rd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation. San Diego: ACM, 2022. 809–824. [doi: 10.1145/3519939.3523432] — [doi:10.1145/3519939.3523432](https://doi.org/10.1145/3519939.3523432) [find](https://scholar.google.com/scholar?q=Mulder+I%2C+Krebbers+R%2C+Geuvers+H%2E+Diaframe%3A+Automated+verification+of+fine%2Dgrained+concurrent+programs+in+Iris%2E+In%3A+Proc%2E+of+the+43rd+ACM+SIGPLAN+Int%E2%80%99l+Conf%2E+on+Programming+Language+Design+and+Implemen)
27. Jung R, Swasey D, Sieczkowski F, Svendsen K. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. ACM SIGPLAN Notices, 2015, 50(1): 637–650. [doi: 10.1145/2775051.2676980] — [doi:10.1145/2775051.2676980](https://doi.org/10.1145/2775051.2676980) [find](https://scholar.google.com/scholar?q=Jung+R%2C+Swasey+D%2C+Sieczkowski+F%2C+Svendsen+K%2E+Iris%3A+Monoids+and+invariants+as+an+orthogonal+basis+for+concurrent+reasoning%2E+ACM+SIGPLAN+Notices%2C+2015%2C+50%281%29%3A+637%E2%80%93650%2E+%5Bdoi%3A+10%2E1145%2F2775051%2E2676980%5D+%E2%80%94+%5B)
28. Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 2018, 28: e20. [doi: 10.1017/S0956796818000151] — [doi:10.1017/s0956796818000151](https://doi.org/10.1017/s0956796818000151) [find](https://scholar.google.com/scholar?q=Jung+R%2C+Krebbers+R%2C+Jourdan+JH%2C+Bizjak+A%2C+Birkedal+L%2C+Dreyer+D%2E+Iris+from+the+ground+up%3A+A+modular+foundation+for+higher%2Dorder+concurrent+separation+logic%2E+Journal+of+Functional+Programming%2C+2018%2C+28%3A)
29. Wolf FA, Schwerhoff M, Müller P. Concise outlines for a complex logic: A proof outline checker for TaDA. Formal Methods in System Design, 2022, 61(1): 110–136. [doi: 10.1007/s10703-023-00427-w] — [doi:10.1007/s10703-023-00427-w](https://doi.org/10.1007/s10703-023-00427-w) [find](https://scholar.google.com/scholar?q=Wolf+FA%2C+Schwerhoff+M%2C+M%C3%BCller+P%2E+Concise+outlines+for+a+complex+logic%3A+A+proof+outline+checker+for+TaDA%2E+Formal+Methods+in+System+Design%2C+2022%2C+61%281%29%3A+110%E2%80%93136%2E+%5Bdoi%3A+10%2E1007%2Fs10703%2D023%2D00427%2Dw%5D+%E2%80%94+%5Bdoi)
30. Müller P, Schwerhoff M, Summers AJ. Viper: A verification infrastructure for permission-based reasoning. In: Proc. of the 17th Int’l Conf. on Verification, Model Checking, and Abstract Interpretation. St. Petersburg: Springer, 2016. 41–62. [doi: 10.1007/978-3-662-49122-5_2] — [doi:10.1007/978-3-662-49122-5_2](https://doi.org/10.1007/978-3-662-49122-5_2) [find](https://scholar.google.com/scholar?q=M%C3%BCller+P%2C+Schwerhoff+M%2C+Summers+AJ%2E+Viper%3A+A+verification+infrastructure+for+permission%2Dbased+reasoning%2E+In%3A+Proc%2E+of+the+17th+Int%E2%80%99l+Conf%2E+on+Verification%2C+Model+Checking%2C+and+Abstract+Interpretation%2E)
31. da Rocha Pinto P, Dinsdale-Young T, Gardner P. TaDA: A logic for time and data abstraction. In: Proc. of the 28th European Conf. on ECOOP 2014—Object-oriented Programming. Uppsala: Springer, 2014. 207–231. [doi: 10.1007/978-3-662-44202-9_9] — [doi:10.1007/978-3-662-44202-9_9](https://doi.org/10.1007/978-3-662-44202-9_9) [find](https://scholar.google.com/scholar?q=da+Rocha+Pinto+P%2C+Dinsdale%2DYoung+T%2C+Gardner+P%2E+TaDA%3A+A+logic+for+time+and+data+abstraction%2E+In%3A+Proc%2E+of+the+28th+European+Conf%2E+on+ECOOP+2014%E2%80%94Object%2Doriented+Programming%2E+Uppsala%3A+Springer%2C+2014%2E+207)
32. Appel AW. Verified software toolchain: (Invited Talk). In: Proc. of the 20th European Symp. on Programming. Saarbrücken: Springer, 2011. 1–17. [doi: 10.1007/978-3-642-19718-5_1] — [doi:10.1007/978-3-642-19718-5_1](https://doi.org/10.1007/978-3-642-19718-5_1) [find](https://scholar.google.com/scholar?q=Appel+AW%2E+Verified+software+toolchain%3A+%28Invited+Talk%29%2E+In%3A+Proc%2E+of+the+20th+European+Symp%2E+on+Programming%2E+Saarbr%C3%BCcken%3A+Springer%2C+2011%2E+1%E2%80%9317%2E+%5Bdoi%3A+10%2E1007%2F978%2D3%2D642%2D19718%2D5%5F1%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2F978%2D3%2D6)
33. Dang HH, Jourdan JH, Kaiser JO, Dreyer D. RustBelt meets relaxed memory. Proc. of the ACM on Programming Languages, 2019, 4: 34. [doi: 10.1145/3371102] — [doi:10.1145/3371102](https://doi.org/10.1145/3371102) [find](https://scholar.google.com/scholar?q=Dang+HH%2C+Jourdan+JH%2C+Kaiser+JO%2C+Dreyer+D%2E+RustBelt+meets+relaxed+memory%2E+Proc%2E+of+the+ACM+on+Programming+Languages%2C+2019%2C+4%3A+34%2E+%5Bdoi%3A+10%2E1145%2F3371102%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F3371102%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1145%2F)
34. Liang HJ, Feng XY, Shao Z. Compositional verification of termination-preserving refinement of concurrent programs. In: Proc. of the 23rd Joint Meeting of the EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). Vienna: ACM, 2014.… — [doi:10.1145/2603088.2603123](https://doi.org/10.1145/2603088.2603123) [find](https://scholar.google.com/scholar?q=Liang+HJ%2C+Feng+XY%2C+Shao+Z%2E+Compositional+verification+of+termination%2Dpreserving+refinement+of+concurrent+programs%2E+In%3A+Proc%2E+of+the+23rd+Joint+Meeting+of+the+EACSL+Annual+Conf%2E+on+Computer+Science+Log)
35. Lamport L. On interprocess communication: Part II: Algorithms. Distributed Computing, 1986, 1(2): 86–101. [doi: 10.1007/BF01786228] — [doi:10.1007/bf01786228](https://doi.org/10.1007/bf01786228) [find](https://scholar.google.com/scholar?q=Lamport+L%2E+On+interprocess+communication%3A+Part+II%3A+Algorithms%2E+Distributed+Computing%2C+1986%2C+1%282%29%3A+86%E2%80%93101%2E+%5Bdoi%3A+10%2E1007%2FBF01786228%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2Fbf01786228%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2Fbf01786228%29)
36. Liang HJ, Feng XY. Modular verification of linearizability with non-fixed linearization points. In: Proc. of the 34th ACM SIGPLAN Conf. on Programming Language Design and Implementation. Seattle: ACM, 2013. 459–470. [doi: 10.1145/2491956.2462189] — [doi:10.1145/2491956.2462189](https://doi.org/10.1145/2491956.2462189) [find](https://scholar.google.com/scholar?q=Liang+HJ%2C+Feng+XY%2E+Modular+verification+of+linearizability+with+non%2Dfixed+linearization+points%2E+In%3A+Proc%2E+of+the+34th+ACM+SIGPLAN+Conf%2E+on+Programming+Language+Design+and+Implementation%2E+Seattle%3A+ACM%2C)
37. Dodds M, Haas A, Kirsch CM. A scalable, correct time-stamped stack. ACM SIGPLAN Notices, 2015, 50(1): 233–246. [doi: 10.1145/2775051.2676963] — [doi:10.1145/2775051.2676963](https://doi.org/10.1145/2775051.2676963) [find](https://scholar.google.com/scholar?q=Dodds+M%2C+Haas+A%2C+Kirsch+CM%2E+A+scalable%2C+correct+time%2Dstamped+stack%2E+ACM+SIGPLAN+Notices%2C+2015%2C+50%281%29%3A+233%E2%80%93246%2E+%5Bdoi%3A+10%2E1145%2F2775051%2E2676963%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F2775051%2E2676963%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1145%2F27)
38. Hendler D, Shavit N, Yerushalmi L. A scalable lock-free stack algorithm. In: Proc. of the 16th Annual ACM Symp. on Parallelism in Algorithms and Architectures. Barcelona: ACM, 2004. 206–215. [doi: 10.1145/1007912.1007944] — [doi:10.1145/1007912.1007944](https://doi.org/10.1145/1007912.1007944) [find](https://scholar.google.com/scholar?q=Hendler+D%2C+Shavit+N%2C+Yerushalmi+L%2E+A+scalable+lock%2Dfree+stack+algorithm%2E+In%3A+Proc%2E+of+the+16th+Annual+ACM+Symp%2E+on+Parallelism+in+Algorithms+and+Architectures%2E+Barcelona%3A+ACM%2C+2004%2E+206%E2%80%93215%2E+%5Bdoi%3A+10%2E)
39. Vindum SF, Frumin D, Birkedal L. Mechanized verification of a fine-grained concurrent queue from meta’s folly library. In: Proc. of the 11th ACM SIGPLAN Int’l Conf. on Certified Programs and Proofs. Philadelphia: ACM, 2022. 100–115. [doi: 10.1145/3497775.3503689] — [doi:10.1145/3497775.3503689](https://doi.org/10.1145/3497775.3503689) [find](https://scholar.google.com/scholar?q=Vindum+SF%2C+Frumin+D%2C+Birkedal+L%2E+Mechanized+verification+of+a+fine%2Dgrained+concurrent+queue+from+meta%E2%80%99s+folly+library%2E+In%3A+Proc%2E+of+the+11th+ACM+SIGPLAN+Int%E2%80%99l+Conf%2E+on+Certified+Programs+and+Proofs%2E+P)
40. Neiger G. Set-linearizability. In: Proc. of the 13th Annual ACM Symp. on Principles of Distributed Computing. Los Angeles: ACM, 1994. [doi: 10.1145/197917.198176] — [doi:10.1145/197917.198176](https://doi.org/10.1145/197917.198176) [find](https://scholar.google.com/scholar?q=Neiger+G%2E+Set%2Dlinearizability%2E+In%3A+Proc%2E+of+the+13th+Annual+ACM+Symp%2E+on+Principles+of+Distributed+Computing%2E+Los+Angeles%3A+ACM%2C+1994%2E+%5Bdoi%3A+10%2E1145%2F197917%2E198176%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F197917%2E198176%5D%28https%3A%2F)
41. Hemed N, Rinetzky N, Vafeiadis V. Modular verification of concurrency-aware linearizability. In: Proc. of the 29th Int’l Symp. on Distributed Computing. Tokyo: Springer, 2015. 371–387. [doi: 10.1007/978-3-662-48653-5_25] — [doi:10.1007/978-3-662-48653-5_25](https://doi.org/10.1007/978-3-662-48653-5_25) [find](https://scholar.google.com/scholar?q=Hemed+N%2C+Rinetzky+N%2C+Vafeiadis+V%2E+Modular+verification+of+concurrency%2Daware+linearizability%2E+In%3A+Proc%2E+of+the+29th+Int%E2%80%99l+Symp%2E+on+Distributed+Computing%2E+Tokyo%3A+Springer%2C+2015%2E+371%E2%80%93387%2E+%5Bdoi%3A+10%2E1007%2F9)
42. Castañeda A, Rajsbaum S, Raynal M. Specifying concurrent problems: Beyond linearizability and up to tasks. In: Proc. of the 29th Int’l Symp. on Distributed Computing. Tokyo: Springer, 2015. 420–435. [doi: 10.1007/978-3-662-48653-5_28] — [doi:10.1007/978-3-662-48653-5_28](https://doi.org/10.1007/978-3-662-48653-5_28) [find](https://scholar.google.com/scholar?q=Casta%C3%B1eda+A%2C+Rajsbaum+S%2C+Raynal+M%2E+Specifying+concurrent+problems%3A+Beyond+linearizability+and+up+to+tasks%2E+In%3A+Proc%2E+of+the+29th+Int%E2%80%99l+Symp%2E+on+Distributed+Computing%2E+Tokyo%3A+Springer%2C+2015%2E+420%E2%80%93435%2E+%5B)
43. Castañeda A, Rajsbaum S, Raynal M. Unifying concurrent objects and distributed tasks: Interval-linearizability. Journal of the ACM, 2018, 65(6): 45. [doi: 10.1145/3266457] — [doi:10.1145/3266457](https://doi.org/10.1145/3266457) [find](https://scholar.google.com/scholar?q=Casta%C3%B1eda+A%2C+Rajsbaum+S%2C+Raynal+M%2E+Unifying+concurrent+objects+and+distributed+tasks%3A+Interval%2Dlinearizability%2E+Journal+of+the+ACM%2C+2018%2C+65%286%29%3A+45%2E+%5Bdoi%3A+10%2E1145%2F3266457%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F3266457%5D%28http)
44. Vale AO, Shao Z, Chen YX. A Compositional theory of linearizability. Proc. of the ACM on Programming Languages, 2023, 7: 1089–1120. [doi: 10.1145/3571231] — [doi:10.1145/3571231](https://doi.org/10.1145/3571231) [find](https://scholar.google.com/scholar?q=Vale+AO%2C+Shao+Z%2C+Chen+YX%2E+A+Compositional+theory+of+linearizability%2E+Proc%2E+of+the+ACM+on+Programming+Languages%2C+2023%2C+7%3A+1089%E2%80%931120%2E+%5Bdoi%3A+10%2E1145%2F3571231%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F3571231%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E11)
45. Lafont Y, Streicher T. Games semantics for linear logic. In: Proc. of the 6th Annual IEEE Symp. on Logic in Computer Science. Amsterdam: IEEE, 1991. 43–50. [doi: 10.1109/LICS.1991.151629] — [doi:10.1109/lics.1991.151629](https://doi.org/10.1109/lics.1991.151629) [find](https://scholar.google.com/scholar?q=Lafont+Y%2C+Streicher+T%2E+Games+semantics+for+linear+logic%2E+In%3A+Proc%2E+of+the+6th+Annual+IEEE+Symp%2E+on+Logic+in+Computer+Science%2E+Amsterdam%3A+IEEE%2C+1991%2E+43%E2%80%9350%2E+%5Bdoi%3A+10%2E1109%2FLICS%2E1991%2E151629%5D+%E2%80%94+%5Bdoi%3A10%2E11)
46. Hyland JME, Ong CHL. On full abstraction for PCF: I, II, and III. Information and Computation, 2000, 163(2): 285–408. [doi: 10.1006/inco.2000.2917] — [doi:10.1006/inco.2000.2917](https://doi.org/10.1006/inco.2000.2917) [find](https://scholar.google.com/scholar?q=Hyland+JME%2C+Ong+CHL%2E+On+full+abstraction+for+PCF%3A+I%2C+II%2C+and+III%2E+Information+and+Computation%2C+2000%2C+163%282%29%3A+285%E2%80%93408%2E+%5Bdoi%3A+10%2E1006%2Finco%2E2000%2E2917%5D+%E2%80%94+%5Bdoi%3A10%2E1006%2Finco%2E2000%2E2917%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E10)
47. Goubault É, Ledent J, Mimram S. Concurrent specifications beyond linearizability. In: Proc. of the 22nd Int’l Conf. on Principles of Distributed Systems (OPODIS 2018). Dagstuhl Publishing, 2018. 28. [find](https://scholar.google.com/scholar?q=Goubault+%C3%89%2C+Ledent+J%2C+Mimram+S%2E+Concurrent+specifications+beyond+linearizability%2E+In%3A+Proc%2E+of+the+22nd+Int%E2%80%99l+Conf%2E+on+Principles+of+Distributed+Systems+%28OPODIS+2018%29%2E+Dagstuhl+Publishing%2C+2018%2E+28%2E)
48. Hoare CAR, Jifeng HE, Sanders JW. Prespecification in data refinement. Information Processing Letters, 1987, 25(2): 71–76. [doi: 10.1016/0020-0190(87)90224-9] — [doi:10.1016/0020-0190(87)90224-9](https://doi.org/10.1016/0020-0190%2887%2990224-9) [find](https://scholar.google.com/scholar?q=Hoare+CAR%2C+Jifeng+HE%2C+Sanders+JW%2E+Prespecification+in+data+refinement%2E+Information+Processing+Letters%2C+1987%2C+25%282%29%3A+71%E2%80%9376%2E+%5Bdoi%3A+10%2E1016%2F0020%2D0190%2887%2990224%2D9%5D+%E2%80%94+%5Bdoi%3A10%2E1016%2F0020%2D0190%2887%2990224%2D9%5D%28http)
49. He J, Hoare CAR, Sanders JW. Data refinement refined resume. In: Proc. of the 1986 European Symp. on Programming. Saarbrücken: Springer, 1986. 187–196. [doi: 10.1007/3-540-16442-1_14] — [doi:10.1007/3-540-16442-1_14](https://doi.org/10.1007/3-540-16442-1_14) [find](https://scholar.google.com/scholar?q=He+J%2C+Hoare+CAR%2C+Sanders+JW%2E+Data+refinement+refined+resume%2E+In%3A+Proc%2E+of+the+1986+European+Symp%2E+on+Programming%2E+Saarbr%C3%BCcken%3A+Springer%2C+1986%2E+187%E2%80%93196%2E+%5Bdoi%3A+10%2E1007%2F3%2D540%2D16442%2D1%5F14%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2F3)
50. Filipović I, O’Hearn P, Rinetzky N, Yang H. Abstraction for concurrent objects. Theoretical Computer Science, 2010, 411(51-52): 4379–4398. [doi: 10.1016/j.tcs.2010.09.021] — [doi:10.1016/j.tcs.2010.09.021](https://doi.org/10.1016/j.tcs.2010.09.021) [find](https://scholar.google.com/scholar?q=Filipovi%C4%87+I%2C+O%E2%80%99Hearn+P%2C+Rinetzky+N%2C+Yang+H%2E+Abstraction+for+concurrent+objects%2E+Theoretical+Computer+Science%2C+2010%2C+411%2851%2D52%29%3A+4379%E2%80%934398%2E+%5Bdoi%3A+10%2E1016%2Fj%2Etcs%2E2010%2E09%2E021%5D+%E2%80%94+%5Bdoi%3A10%2E1016%2Fj%2Etcs%2E2010%2E09)
51. Frumin D, Krebbers R, Birkedal L. ReLoC: A mechanised relational logic for fine-grained concurrency. In: Proc. of the 33rd Annual ACM/IEEE Symp. on Logic in Computer Science. Oxford: ACM, 2018. 442–451. [doi: 10.1145/3209108.3209174] — [doi:10.1145/3209108.3209174](https://doi.org/10.1145/3209108.3209174) [find](https://scholar.google.com/scholar?q=Frumin+D%2C+Krebbers+R%2C+Birkedal+L%2E+ReLoC%3A+A+mechanised+relational+logic+for+fine%2Dgrained+concurrency%2E+In%3A+Proc%2E+of+the+33rd+Annual+ACM%2FIEEE+Symp%2E+on+Logic+in+Computer+Science%2E+Oxford%3A+ACM%2C+2018%2E+442%E2%80%9345)
52. Turon AJ, Thamsborg J, Ahmed A, Birkedal L, Dreyer D. Logical relations for fine-grained concurrency. ACM SIGPLAN Notices, 2013, 48(1): 343–356. [doi: 10.1145/2480359.2429111] — [doi:10.1145/2480359.2429111](https://doi.org/10.1145/2480359.2429111) [find](https://scholar.google.com/scholar?q=Turon+AJ%2C+Thamsborg+J%2C+Ahmed+A%2C+Birkedal+L%2C+Dreyer+D%2E+Logical+relations+for+fine%2Dgrained+concurrency%2E+ACM+SIGPLAN+Notices%2C+2013%2C+48%281%29%3A+343%E2%80%93356%2E+%5Bdoi%3A+10%2E1145%2F2480359%2E2429111%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F2480359%2E2)
53. Plotkin GD. Lambda-definability and Logical Relations. Technical Report, Edinburgh: University of Edinburgh, 1973. [https://www.cl.cam.ac.uk/~nk480/plotkin-logical-relations.pdf](https://www.cl.cam.ac.uk/~nk480/plotkin-logical-relations.pdf) [↗](https://www.cl.cam.ac.uk/~nk480/plotkin-logical-relations.pdf)
54. Xu FW, Fu M, Feng XY, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernels. In: Proc. of the 28th Int’l Conf. on Computer Aided Verification. Toronto: Springer, 2016. 59–79. [doi: 10.1007/978-3-319-41540-6_4] — [doi:10.1007/978-3-319-41540-6_4](https://doi.org/10.1007/978-3-319-41540-6_4) [find](https://scholar.google.com/scholar?q=Xu+FW%2C+Fu+M%2C+Feng+XY%2C+Zhang+XR%2C+Zhang+H%2C+Li+ZH%2E+A+practical+verification+framework+for+preemptive+OS+kernels%2E+In%3A+Proc%2E+of+the+28th+Int%E2%80%99l+Conf%2E+on+Computer+Aided+Verification%2E+Toronto%3A+Springer%2C+2016%2E)
55. Gäher L, Sammler M, Spies S, Jung R, Dang HH, Krebbers R, Kang J, Dreyer D. Simuliris: A separation logic framework for verifying concurrent program optimizations. Proc. of the ACM on Programming Languages, 2022, 6: 28. [doi: 10.1145/3498689] — [doi:10.1145/3498689](https://doi.org/10.1145/3498689) [find](https://scholar.google.com/scholar?q=G%C3%A4her+L%2C+Sammler+M%2C+Spies+S%2C+Jung+R%2C+Dang+HH%2C+Krebbers+R%2C+Kang+J%2C+Dreyer+D%2E+Simuliris%3A+A+separation+logic+framework+for+verifying+concurrent+program+optimizations%2E+Proc%2E+of+the+ACM+on+Programming+Lang)
56. Liang HJ, Feng XY, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In: Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Philadelphia: ACM, 2012. 455–468. [doi: 10.1145/2103656.2103711] — [doi:10.1145/2103656.2103711](https://doi.org/10.1145/2103656.2103711) [find](https://scholar.google.com/scholar?q=Liang+HJ%2C+Feng+XY%2C+Fu+M%2E+A+rely%2Dguarantee%2Dbased+simulation+for+verifying+concurrent+program+transformations%2E+In%3A+Proc%2E+of+the+39th+Annual+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Language)
57. Herlihy M, Shavit N, Luchangco V, et al. The art of multiprocessor programming. Newnes, 2020. 54–55. [https://www.sciencedirect.com/book/9780124159501/the-art-of-multiprocessor-programming](https://www.sciencedirect.com/book/9780124159501/the-art-of-multiprocessor-programming) [↗](https://www.sciencedirect.com/book/9780124159501/the-art-of-multiprocessor-programming)
58. Svendsen K, Birkedal L, Parkinson M. Modular reasoning about separation of concurrent data structures. In: Proc. of the 22nd European Symp. on Programming. Rome: Springer, 2013. 169–188. [doi: 10.1007/978-3-642-37036-6_11] — [doi:10.1007/978-3-642-37036-6_11](https://doi.org/10.1007/978-3-642-37036-6_11) [find](https://scholar.google.com/scholar?q=Svendsen+K%2C+Birkedal+L%2C+Parkinson+M%2E+Modular+reasoning+about+separation+of+concurrent+data+structures%2E+In%3A+Proc%2E+of+the+22nd+European+Symp%2E+on+Programming%2E+Rome%3A+Springer%2C+2013%2E+169%E2%80%93188%2E+%5Bdoi%3A+10%2E1007)
59. O'Hearn PW, Yang H, Reynolds JC. Separation and information hiding. In: Proc. of the 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Venice: ACM, 2004. 268–280. [doi: 10.1145/964001.964024] — [doi:10.1145/964001.964024](https://doi.org/10.1145/964001.964024) [find](https://scholar.google.com/scholar?q=O%27Hearn+PW%2C+Yang+H%2C+Reynolds+JC%2E+Separation+and+information+hiding%2E+In%3A+Proc%2E+of+the+31st+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Languages%2E+Venice%3A+ACM%2C+2004%2E+268%E2%80%93280%2E+%5Bdoi%3A+10%2E1145%2F964)
60. Cook SA. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 1978, 7(1): 70–90. [doi: 10.1137/0207005] — [doi:10.1137/0207005](https://doi.org/10.1137/0207005) [find](https://scholar.google.com/scholar?q=Cook+SA%2E+Soundness+and+completeness+of+an+axiom+system+for+program+verification%2E+SIAM+Journal+on+Computing%2C+1978%2C+7%281%29%3A+70%E2%80%9390%2E+%5Bdoi%3A+10%2E1137%2F0207005%5D+%E2%80%94+%5Bdoi%3A10%2E1137%2F0207005%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1137%2F02)
61. O’Hearn P, Reynolds J, Yang H. Local reasoning about programs that alter data structures. In: Proc. of the 15th Int’l Workshop on Computer Science Logic. Paris: Springer, 2001. 1–19. [doi: 10.1007/3-540-44802-0_1] — [doi:10.1007/3-540-44802-0_1](https://doi.org/10.1007/3-540-44802-0_1) [find](https://scholar.google.com/scholar?q=O%E2%80%99Hearn+P%2C+Reynolds+J%2C+Yang+H%2E+Local+reasoning+about+programs+that+alter+data+structures%2E+In%3A+Proc%2E+of+the+15th+Int%E2%80%99l+Workshop+on+Computer+Science+Logic%2E+Paris%3A+Springer%2C+2001%2E+1%E2%80%9319%2E+%5Bdoi%3A+10%2E1007%2F3%2D5)
62. Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science. Copenhagen: IEEE, 2002. 55–74. [doi: 10.1109/LICS.2002.1029817] — [doi:10.1109/lics.2002.1029817](https://doi.org/10.1109/lics.2002.1029817) [find](https://scholar.google.com/scholar?q=Reynolds+JC%2E+Separation+logic%3A+A+logic+for+shared+mutable+data+structures%2E+In%3A+Proc%2E+of+the+17th+Annual+IEEE+Symp%2E+on+Logic+in+Computer+Science%2E+Copenhagen%3A+IEEE%2C+2002%2E+55%E2%80%9374%2E+%5Bdoi%3A+10%2E1109%2FLICS%2E2002%2E)
63. Brookes S. A semantics for concurrent separation logic. Theoretical Computer Science, 2007, 375(1–3): 227–270. [doi: 10.1016/j.tcs.2006.12.034] — [doi:10.1016/j.tcs.2006.12.034](https://doi.org/10.1016/j.tcs.2006.12.034) [find](https://scholar.google.com/scholar?q=Brookes+S%2E+A+semantics+for+concurrent+separation+logic%2E+Theoretical+Computer+Science%2C+2007%2C+375%281%E2%80%933%29%3A+227%E2%80%93270%2E+%5Bdoi%3A+10%2E1016%2Fj%2Etcs%2E2006%2E12%2E034%5D+%E2%80%94+%5Bdoi%3A10%2E1016%2Fj%2Etcs%2E2006%2E12%2E034%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E101)
64. Owicki S, Gries D. Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM, 1976, 19(5): 279–285. [doi: 10.1145/360051.360224] — [doi:10.1145/360051.360224](https://doi.org/10.1145/360051.360224) [find](https://scholar.google.com/scholar?q=Owicki+S%2C+Gries+D%2E+Verifying+properties+of+parallel+programs%3A+An+axiomatic+approach%2E+Communications+of+the+ACM%2C+1976%2C+19%285%29%3A+279%E2%80%93285%2E+%5Bdoi%3A+10%2E1145%2F360051%2E360224%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F360051%2E360224%5D%28https%3A%2F)
65. Svendsen K, Birkedal L. Impredicative concurrent abstract predicates. In: Proc. of the 23rd European Symp. on Programming. Grenoble: Springer, 2014. 149–168. [doi: 10.1007/978-3-642-54833-8_9] — [doi:10.1007/978-3-642-54833-8_9](https://doi.org/10.1007/978-3-642-54833-8_9) [find](https://scholar.google.com/scholar?q=Svendsen+K%2C+Birkedal+L%2E+Impredicative+concurrent+abstract+predicates%2E+In%3A+Proc%2E+of+the+23rd+European+Symp%2E+on+Programming%2E+Grenoble%3A+Springer%2C+2014%2E+149%E2%80%93168%2E+%5Bdoi%3A+10%2E1007%2F978%2D3%2D642%2D54833%2D8%5F9%5D+%E2%80%94+%5Bdoi%3A)
66. Alfieri RA. An efficient kernel-based implementation of POSIX threads. In: Proc. of the 1994 USENIX Summer Technical Conf. on USENIX Summer 1994 Technical Conf. Boston: USENIX Association, 1994. 59–72. [find](https://scholar.google.com/scholar?q=Alfieri+RA%2E+An+efficient+kernel%2Dbased+implementation+of+POSIX+threads%2E+In%3A+Proc%2E+of+the+1994+USENIX+Summer+Technical+Conf%2E+on+USENIX+Summer+1994+Technical+Conf%2E+Boston%3A+USENIX+Association%2C+1994%2E+59%E2%80%9372)
67. The OpenMP API specifcation for parallel programming, 2020. [https://www.openmp.org/wp-content/uploads/OpenMP-API-Specification-5-2](https://www.openmp.org/wp-content/uploads/OpenMP-API-Specification-5-2) [↗](https://www.openmp.org/wp-content/uploads/OpenMP-API-Specification-5-2)
68. Gotsman A, Berdine J, Cook B, Rinetzky N, Sagiv M. Local reasoning for storable locks and threads. In: Proc. of the 5th Asian Conf. on Programming Languages and Systems. Singapore: Springer, 2007. 19–37. [doi: 10.1007/978-3-540-76637-7_3] — [doi:10.1007/978-3-540-76637-7_3](https://doi.org/10.1007/978-3-540-76637-7_3) [find](https://scholar.google.com/scholar?q=Gotsman+A%2C+Berdine+J%2C+Cook+B%2C+Rinetzky+N%2C+Sagiv+M%2E+Local+reasoning+for+storable+locks+and+threads%2E+In%3A+Proc%2E+of+the+5th+Asian+Conf%2E+on+Programming+Languages+and+Systems%2E+Singapore%3A+Springer%2C+2007%2E+19%E2%80%93)
69. Feng XY. Local rely-guarantee reasoning. In: Proc. of the 36th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Savannah: ACM, 2009. 315–327. [doi: 10.1145/1480881.1480922] — [doi:10.1145/1480881.1480922](https://doi.org/10.1145/1480881.1480922) [find](https://scholar.google.com/scholar?q=Feng+XY%2E+Local+rely%2Dguarantee+reasoning%2E+In%3A+Proc%2E+of+the+36th+Annual+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Languages%2E+Savannah%3A+ACM%2C+2009%2E+315%E2%80%93327%2E+%5Bdoi%3A+10%2E1145%2F1480881%2E1480922%5D+%E2%80%94+%5Bd)
70. Dodds M, Feng X, Parkinson M, Vafeiadis V. Deny-guarantee reasoning. In: Proc. of the 18th European Symp. on Programming. York: Springer, 2009. 363–377. [doi: 10.1007/978-3-642-00590-9_26] — [doi:10.1007/978-3-642-00590-9_26](https://doi.org/10.1007/978-3-642-00590-9_26) [find](https://scholar.google.com/scholar?q=Dodds+M%2C+Feng+X%2C+Parkinson+M%2C+Vafeiadis+V%2E+Deny%2Dguarantee+reasoning%2E+In%3A+Proc%2E+of+the+18th+European+Symp%2E+on+Programming%2E+York%3A+Springer%2C+2009%2E+363%E2%80%93377%2E+%5Bdoi%3A+10%2E1007%2F978%2D3%2D642%2D00590%2D9%5F26%5D+%E2%80%94+%5Bdoi%3A10%2E1)
71. Dreyer D, Neis G, Rossberg A, Birkedal L. A relational modal logic for higher-order stateful ADTs. In: Proc. of the 37th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Madrid: Springer, 2010. 185–198. [doi: 10.1145/1706299.1706323] — [doi:10.1145/1706299.1706323](https://doi.org/10.1145/1706299.1706323) [find](https://scholar.google.com/scholar?q=Dreyer+D%2C+Neis+G%2C+Rossberg+A%2C+Birkedal+L%2E+A+relational+modal+logic+for+higher%2Dorder+stateful+ADTs%2E+In%3A+Proc%2E+of+the+37th+Annual+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Languages%2E+Madrid%3A)
72. Ahmed A, Dreyer D, Rossberg A. State-dependent representation independence. ACM SIGPLAN Notices, 2009, 44(1): 340–353. [doi: 10.1145/1594834.1480925] — [doi:10.1145/1594834.1480925](https://doi.org/10.1145/1594834.1480925) [find](https://scholar.google.com/scholar?q=Ahmed+A%2C+Dreyer+D%2C+Rossberg+A%2E+State%2Ddependent+representation+independence%2E+ACM+SIGPLAN+Notices%2C+2009%2C+44%281%29%3A+340%E2%80%93353%2E+%5Bdoi%3A+10%2E1145%2F1594834%2E1480925%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F1594834%2E1480925%5D%28https%3A%2F%2Fdoi%2Eorg%2F10)
73. Pitts AM, Stark IDB. Operational reasoning for functions with local state. In: Higher Order Operational Techniques in Semantics. Cambridge: Cambridge University Press, 1999. 227–274. [find](https://scholar.google.com/scholar?q=Pitts+AM%2C+Stark+IDB%2E+Operational+reasoning+for+functions+with+local+state%2E+In%3A+Higher+Order+Operational+Techniques+in+Semantics%2E+Cambridge%3A+Cambridge+University+Press%2C+1999%2E+227%E2%80%93274%2E)
74. Frumin D, Krebbers R, Birkedal L. ReLoC reloaded: A mechanized relational logic for fine-grained concurrency and logical atomicity. arXiv: 2006.13635, 2021. — [arXiv:2006.13635](https://arxiv.org/abs/2006.13635) [find](https://scholar.google.com/scholar?q=Frumin+D%2C+Krebbers+R%2C+Birkedal+L%2E+ReLoC+reloaded%3A+A+mechanized+relational+logic+for+fine%2Dgrained+concurrency+and+logical+atomicity%2E+arXiv%3A+2006%2E13635%2C+2021%2E+%E2%80%94+%5BarXiv%3A2006%2E13635%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F)
75. Turon A, Dreyer D, Birkedal L. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In: Proc. of the 18th ACM SIGPLAN Int’l Conf. on Functional Programming. Boston: ACM, 2013. 377–390. [doi: 10.1145/2500365.2500600] — [doi:10.1145/2500365.2500600](https://doi.org/10.1145/2500365.2500600) [find](https://scholar.google.com/scholar?q=Turon+A%2C+Dreyer+D%2C+Birkedal+L%2E+Unifying+refinement+and+Hoare%2Dstyle+reasoning+in+a+logic+for+higher%2Dorder+concurrency%2E+In%3A+Proc%2E+of+the+18th+ACM+SIGPLAN+Int%E2%80%99l+Conf%2E+on+Functional+Programming%2E+Boston%3A+A)
76. Mulder I, Krebbers R. Proof automation for linearizability in separation logic. Proc. of the ACM on Programming Languages, 2023, 7: 462–491. [doi: 10.1145/3586043] — [doi:10.1145/3586043](https://doi.org/10.1145/3586043) [find](https://scholar.google.com/scholar?q=Mulder+I%2C+Krebbers+R%2E+Proof+automation+for+linearizability+in+separation+logic%2E+Proc%2E+of+the+ACM+on+Programming+Languages%2C+2023%2C+7%3A+462%E2%80%93491%2E+%5Bdoi%3A+10%2E1145%2F3586043%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F3586043%5D%28https%3A%2F%2Fdoi%2E)
77. Khyzha A, Dodds M, Gotsman A, Parkinson M. Proving linearizability using partial orders. In: Proc. of the 26th European Symp. on Programming. Uppsala: Springer, 2017. 639–667. [doi: 10.1007/978-3-662-54434-1_24] — [doi:10.1007/978-3-662-54434-1_24](https://doi.org/10.1007/978-3-662-54434-1_24) [find](https://scholar.google.com/scholar?q=Khyzha+A%2C+Dodds+M%2C+Gotsman+A%2C+Parkinson+M%2E+Proving+linearizability+using+partial+orders%2E+In%3A+Proc%2E+of+the+26th+European+Symp%2E+on+Programming%2E+Uppsala%3A+Springer%2C+2017%2E+639%E2%80%93667%2E+%5Bdoi%3A+10%2E1007%2F978%2D3%2D662%2D)
78. Khyzha A, Gotsman A, Parkinson M. A generic logic for proving linearizability. In: Proc. of the 21st Int’l Symp. Limassol: Springer Int’l Publishing—FM 2016: Formal Methods. 2016. 426–443. [doi: 10.1007/978-3-319-48989-6_26] — [doi:10.1007/978-3-319-48989-6_26](https://doi.org/10.1007/978-3-319-48989-6_26) [find](https://scholar.google.com/scholar?q=Khyzha+A%2C+Gotsman+A%2C+Parkinson+M%2E+A+generic+logic+for+proving+linearizability%2E+In%3A+Proc%2E+of+the+21st+Int%E2%80%99l+Symp%2E+Limassol%3A+Springer+Int%E2%80%99l+Publishing%E2%80%94FM+2016%3A+Formal+Methods%2E+2016%2E+426%E2%80%93443%2E+%5Bdoi%3A+10%2E10)
79. Jung R, Lepigre R, Parthasarathy G, Rapoport M, Timany A, Dreyer D, Jacobs B. The future is ours: Prophecy variables in separation logic. Proc. of the ACM on Programming Languages, 2019, 4: 45. [doi: 10.1145/3371113] — [doi:10.1145/3371113](https://doi.org/10.1145/3371113) [find](https://scholar.google.com/scholar?q=Jung+R%2C+Lepigre+R%2C+Parthasarathy+G%2C+Rapoport+M%2C+Timany+A%2C+Dreyer+D%2C+Jacobs+B%2E+The+future+is+ours%3A+Prophecy+variables+in+separation+logic%2E+Proc%2E+of+the+ACM+on+Programming+Languages%2C+2019%2C+4%3A+45%2E+%5Bdoi%3A+)
80. Vafeiadis V, Parkinson M. A marriage of rely/guarantee and separation logic. In: Proc. of the 18th Int’l Conf. on CONCUR 2007—Concurrency Theory. Lisbon: Springer, 2007. 256–271. [doi: 10.1007/978-3-540-74407-8_18] — [doi:10.1007/978-3-540-74407-8_18](https://doi.org/10.1007/978-3-540-74407-8_18) [find](https://scholar.google.com/scholar?q=Vafeiadis+V%2C+Parkinson+M%2E+A+marriage+of+rely%2Fguarantee+and+separation+logic%2E+In%3A+Proc%2E+of+the+18th+Int%E2%80%99l+Conf%2E+on+CONCUR+2007%E2%80%94Concurrency+Theory%2E+Lisbon%3A+Springer%2C+2007%2E+256%E2%80%93271%2E+%5Bdoi%3A+10%2E1007%2F978%2D3%2D5)
81. Sergey I, Nanevski A, Banerjee A. Mechanized verification of fine-grained concurrent programs. In: Proc. of the 36th ACM SIGPLAN Conf. on Programming Language Design and Implementation. Portland: ACM, 2015. 77–87. [doi: 10.1145/2737924.2737964] — [doi:10.1145/2737924.2737964](https://doi.org/10.1145/2737924.2737964) [find](https://scholar.google.com/scholar?q=Sergey+I%2C+Nanevski+A%2C+Banerjee+A%2E+Mechanized+verification+of+fine%2Dgrained+concurrent+programs%2E+In%3A+Proc%2E+of+the+36th+ACM+SIGPLAN+Conf%2E+on+Programming+Language+Design+and+Implementation%2E+Portland%3A+ACM%2C)
82. Mansky W. Bringing Iris into the verified software toolchain. arXiv: 2207.06574, 2022. — [arXiv:2207.06574](https://arxiv.org/abs/2207.06574) [find](https://scholar.google.com/scholar?q=Mansky+W%2E+Bringing+Iris+into+the+verified+software+toolchain%2E+arXiv%3A+2207%2E06574%2C+2022%2E+%E2%80%94+%5BarXiv%3A2207%2E06574%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2207%2E06574%29)
83. Sanán D, Zhao YW, Hou Z, Zhang FY, Tiu A, Liu Y. CSimpl: A rely-guarantee-based framework for verifying concurrent programs. In: Proc. of the 23rd Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Uppsala: Springer, 2017. 481–498. [doi: 10.1007/978-3-662-54577-5_28] — [doi:10.1007/978-3-662-54577-5_28](https://doi.org/10.1007/978-3-662-54577-5_28) [find](https://scholar.google.com/scholar?q=San%C3%A1n+D%2C+Zhao+YW%2C+Hou+Z%2C+Zhang+FY%2C+Tiu+A%2C+Liu+Y%2E+CSimpl%3A+A+rely%2Dguarantee%2Dbased+framework+for+verifying+concurrent+programs%2E+In%3A+Proc%2E+of+the+23rd+Int%E2%80%99l+Conf%2E+on+Tools+and+Algorithms+for+the+Construct)
84. Ni ZZ, Shao Z. Certified assembly programming with embedded code pointers. In: Proc. of the 33rd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Charleston: ACM, 2006. 320–333. [doi: 10.1145/1111037.1111066] — [doi:10.1145/1111037.1111066](https://doi.org/10.1145/1111037.1111066) [find](https://scholar.google.com/scholar?q=Ni+ZZ%2C+Shao+Z%2E+Certified+assembly+programming+with+embedded+code+pointers%2E+In%3A+Proc%2E+of+the+33rd+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Languages%2E+Charleston%3A+ACM%2C+2006%2E+320%E2%80%93333%2E+%5Bdoi%3A+)
85. Jung R, Jourdan JH, Krebbers R, Dreyer D. RustBelt: Securing the foundations of the Rust programming language. Proc. of the ACM on Programming Languages, 2017, 2: 66. [doi: 10.1145/3158154] [find](https://scholar.google.com/scholar?q=Jung+R%2C+Jourdan+JH%2C+Krebbers+R%2C+Dreyer+D%2E+RustBelt%3A+Securing+the+foundations+of+the+Rust+programming+language%2E+Proc%2E+of+the+ACM+on+Programming+Languages%2C+2017%2C+2%3A+66%2E+%5Bdoi%3A+10%2E1145%2F3158154%5D)
86. Matsakis ND, Klock FS. The Rust language. ACM SIGAda Ada Letters, 2014, 34(3): 103–104. [doi: 10.1145/2692956.2663188] — [doi:10.1145/2692956.2663188](https://doi.org/10.1145/2692956.2663188) [find](https://scholar.google.com/scholar?q=Matsakis+ND%2C+Klock+FS%2E+The+Rust+language%2E+ACM+SIGAda+Ada+Letters%2C+2014%2C+34%283%29%3A+103%E2%80%93104%2E+%5Bdoi%3A+10%2E1145%2F2692956%2E2663188%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F2692956%2E2663188%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1145%2F2692956%2E2663188%29)
87. Matsushita Y, Tsukada T, Kobayashi N. RustHorn: CHC-based verification for Rust programs. ACM Trans. on Programming Languages and Systems, 2021, 43(4): 15. [doi: 10.1145/3462205] — [doi:10.1145/3462205](https://doi.org/10.1145/3462205) [find](https://scholar.google.com/scholar?q=Matsushita+Y%2C+Tsukada+T%2C+Kobayashi+N%2E+RustHorn%3A+CHC%2Dbased+verification+for+Rust+programs%2E+ACM+Trans%2E+on+Programming+Languages+and+Systems%2C+2021%2C+43%284%29%3A+15%2E+%5Bdoi%3A+10%2E1145%2F3462205%5D+%E2%80%94+%5Bdoi%3A10%2E1145%2F346220)
88. Matsushita Y, Denis X, Jourdan JH, Dreyer D. RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code. In: Proc. of the 43rd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation. San Diego: ACM, 2022. 841–856. [doi: 10.1145/3519939.352370… — [doi:10.1145/3519939.3523704](https://doi.org/10.1145/3519939.3523704) [find](https://scholar.google.com/scholar?q=Matsushita+Y%2C+Denis+X%2C+Jourdan+JH%2C+Dreyer+D%2E+RustHornBelt%3A+A+semantic+foundation+for+functional+verification+of+Rust+programs+with+unsafe+code%2E+In%3A+Proc%2E+of+the+43rd+ACM+SIGPLAN+Int%E2%80%99l+Conf%2E+on+Program)
89. Chajed T, Tassarotti J, Kaashoek MF, Zeldovich N. Verifying concurrent, crash-safe systems with Perennial. In: Proc. of the 27th ACM Symp. on Operating Systems Principles. Huntsville: ACM, 2019. 243–258. [doi: 10.1145/3341301.3359632] — [doi:10.1145/3341301.3359632](https://doi.org/10.1145/3341301.3359632) [find](https://scholar.google.com/scholar?q=Chajed+T%2C+Tassarotti+J%2C+Kaashoek+MF%2C+Zeldovich+N%2E+Verifying+concurrent%2C+crash%2Dsafe+systems+with+Perennial%2E+In%3A+Proc%2E+of+the+27th+ACM+Symp%2E+on+Operating+Systems+Principles%2E+Huntsville%3A+ACM%2C+2019%2E+243%E2%80%932)
90. Donovan AAA, Kernighan BW. The Go Programming Language. Addison-Wesley Professional, 2015. [find](https://scholar.google.com/scholar?q=Donovan+AAA%2C+Kernighan+BW%2E+The+Go+Programming+Language%2E+Addison%2DWesley+Professional%2C+2015%2E)
91. Chen HG, Ziegler D, Chajed T, Chlipala A, Kaashoek MF, Zeldovich N. Using Crash Hoare logic for certifying the FSCQ file system. In: Proc. of the 25th Symp. on Operating Systems Principles. Monterey: ACM, 2015. 18–37. [doi: 10.1145/2815400.2815402] — [doi:10.1145/2815400.2815402](https://doi.org/10.1145/2815400.2815402) [find](https://scholar.google.com/scholar?q=Chen+HG%2C+Ziegler+D%2C+Chajed+T%2C+Chlipala+A%2C+Kaashoek+MF%2C+Zeldovich+N%2E+Using+Crash+Hoare+logic+for+certifying+the+FSCQ+file+system%2E+In%3A+Proc%2E+of+the+25th+Symp%2E+on+Operating+Systems+Principles%2E+Monterey%3A+)
92. Chajed T, Tassarotti J, Theng M, Jung R. GoJournal: A verified, concurrent, crash-safe journaling system. In: Proc. of the 15th USENIX Symp. on Operating Systems Design and Implementation. USENIX Association, 2021. 423–439. [find](https://scholar.google.com/scholar?q=Chajed+T%2C+Tassarotti+J%2C+Theng+M%2C+Jung+R%2E+GoJournal%3A+A+verified%2C+concurrent%2C+crash%2Dsafe+journaling+system%2E+In%3A+Proc%2E+of+the+15th+USENIX+Symp%2E+on+Operating+Systems+Design+and+Implementation%2E+USENIX+Asso)
93. Sammler M, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. RefinedC: Automating the foundational verification of C code with refined ownership types. In: Proc. of the 42nd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation. Virtual: ACM, 2021. 158–174. [doi: 10.1145/34534… — [doi:10.1145/3453483.3454036](https://doi.org/10.1145/3453483.3454036) [find](https://scholar.google.com/scholar?q=Sammler+M%2C+Lepigre+R%2C+Krebbers+R%2C+Memarian+K%2C+Dreyer+D%2C+Garg+D%2E+RefinedC%3A+Automating+the+foundational+verification+of+C+code+with+refined+ownership+types%2E+In%3A+Proc%2E+of+the+42nd+ACM+SIGPLAN+Int%E2%80%99l+Conf%2E)
94. Leroy X, Blazy S, Kästner D, Schommer B, Pister M, Ferdinand C. CompCert—A formally verified optimizing compiler. In: Proc. of the 8th European Congress of Embedded Real Time Software and Systems (ERTS 2016). Toulouse, 2016. [https://inria.hal.science/hal-01238879/document](https://inria.hal.science/hal-01238879/document) [↗](https://inria.hal.science/hal-01238879/document)
95. Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: Formal verification of an OS kernel. In: Proc. of the 22nd ACM SIGOPS Symp. on Operating Systems Principles. Big Sky: ACM, 2009. 207–220. [doi: 10.1145… [find](https://scholar.google.com/scholar?q=Klein+G%2C+Elphinstone+K%2C+Heiser+G%2C+Andronick+J%2C+Cock+D%2C+Derrin+P%2C+Elkaduwe+D%2C+Engelhardt+K%2C+Kolanski+R%2C+Norrish+M%2C+Sewell+T%2C+Tuch+H%2C+Winwood+S%2E+seL4%3A+Formal+verification+of+an+OS+kernel%2E+In%3A+Proc%2E+of+t)
96. Tuch H, Klein G, Norrish M. Types, bytes, and separation logic. In: Proc. of the 34th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Nice: ACM, 2007. 97–108. [doi: 10.1145/1190216.1190234] — [doi:10.1145/1190216.1190234](https://doi.org/10.1145/1190216.1190234) [find](https://scholar.google.com/scholar?q=Tuch+H%2C+Klein+G%2C+Norrish+M%2E+Types%2C+bytes%2C+and+separation+logic%2E+In%3A+Proc%2E+of+the+34th+Annual+ACM+SIGPLAN%2DSIGACT+Symp%2E+on+Principles+of+Programming+Languages%2E+Nice%3A+ACM%2C+2007%2E+97%E2%80%93108%2E+%5Bdoi%3A+10%2E1145%2F119)
97. Sanan D, Zhao YW, Lin SW, Yang L. CSim 2 : Compositional top-down verification of concurrent systems using rely-guarantee. ACM Trans. on Programming Languages and Systems, 2021, 43(1): 2. [doi: 10.1145/3436808] — [doi:10.1145/3436808](https://doi.org/10.1145/3436808) [find](https://scholar.google.com/scholar?q=Sanan+D%2C+Zhao+YW%2C+Lin+SW%2C+Yang+L%2E+CSim+2+%3A+Compositional+top%2Ddown+verification+of+concurrent+systems+using+rely%2Dguarantee%2E+ACM+Trans%2E+on+Programming+Languages+and+Systems%2C+2021%2C+43%281%29%3A+2%2E+%5Bdoi%3A+10%2E114)
98. Zhao YW, Sanán D, Zhang F, Liu Y. A parametric rely-guarantee reasoning framework for concurrent reactive systems. In: Proc. of the 3rd World Congress on Formal Methods. Porto: Springer, 2019. 161–178. [doi: 10.1007/978-3-030-30942-8_11] — [doi:10.1007/978-3-030-30942-8_11](https://doi.org/10.1007/978-3-030-30942-8_11) [find](https://scholar.google.com/scholar?q=Zhao+YW%2C+San%C3%A1n+D%2C+Zhang+F%2C+Liu+Y%2E+A+parametric+rely%2Dguarantee+reasoning+framework+for+concurrent+reactive+systems%2E+In%3A+Proc%2E+of+the+3rd+World+Congress+on+Formal+Methods%2E+Porto%3A+Springer%2C+2019%2E+161%E2%80%93178)
99. Nieto LP. The rely-guarantee method in Isabelle/HOL. In: Proc. of the 12th European Symp. on Programming. Warsaw: Springer, 2003. 348–362. [doi: 10.1007/3-540-36575-3_24] — [doi:10.1007/3-540-36575-3_24](https://doi.org/10.1007/3-540-36575-3_24) [find](https://scholar.google.com/scholar?q=Nieto+LP%2E+The+rely%2Dguarantee+method+in+Isabelle%2FHOL%2E+In%3A+Proc%2E+of+the+12th+European+Symp%2E+on+Programming%2E+Warsaw%3A+Springer%2C+2003%2E+348%E2%80%93362%2E+%5Bdoi%3A+10%2E1007%2F3%2D540%2D36575%2D3%5F24%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2F3%2D540%2D36575%2D3%5F)
100. Zhao YW, Sanán D. Rely-guarantee reasoning about concurrent memory management in zephyr RTOS. In: Proc. of the 31st Int’l Conf. on Computer Aided Verification. New York City: Springer, 2019. 515–533. [doi: 10.1007/978-3-030-25543-5_29] — [doi:10.1007/978-3-030-25543-5_29](https://doi.org/10.1007/978-3-030-25543-5_29) [find](https://scholar.google.com/scholar?q=Zhao+YW%2C+San%C3%A1n+D%2E+Rely%2Dguarantee+reasoning+about+concurrent+memory+management+in+zephyr+RTOS%2E+In%3A+Proc%2E+of+the+31st+Int%E2%80%99l+Conf%2E+on+Computer+Aided+Verification%2E+New+York+City%3A+Springer%2C+2019%2E+515%E2%80%93533%2E+)
101. Labrosse J. MicroC/OS-II: The Real Time Kernel. CRC Press, 2002. [find](https://scholar.google.com/scholar?q=Labrosse+J%2E+MicroC%2FOS%2DII%3A+The+Real+Time+Kernel%2E+CRC+Press%2C+2002%2E)
102. Zou M, Ding HR, Du D, Fu M, Gu RH, Chen HB. Using concurrent relational logic with helpers for verifying the AtomFS file system. In: Proc. of the 27th ACM Symp. on Operating Systems Principles. Huntsville: ACM, 2019. 259–274. [doi: 10.1145/3341301.3359644] — [doi:10.1145/3341301.3359644](https://doi.org/10.1145/3341301.3359644) [find](https://scholar.google.com/scholar?q=Zou+M%2C+Ding+HR%2C+Du+D%2C+Fu+M%2C+Gu+RH%2C+Chen+HB%2E+Using+concurrent+relational+logic+with+helpers+for+verifying+the+AtomFS+file+system%2E+In%3A+Proc%2E+of+the+27th+ACM+Symp%2E+on+Operating+Systems+Principles%2E+Huntsv)
103. Babaoğlu Ö, Marzullo K, Schneider FB. A formalization of priority inversion. Real-time Systems, 1993, 5(4): 285–303. [doi: 10.1007/BF01088832] — [doi:10.1007/bf01088832](https://doi.org/10.1007/bf01088832) [find](https://scholar.google.com/scholar?q=Babao%C4%9Flu+%C3%96%2C+Marzullo+K%2C+Schneider+FB%2E+A+formalization+of+priority+inversion%2E+Real%2Dtime+Systems%2C+1993%2C+5%284%29%3A+285%E2%80%93303%2E+%5Bdoi%3A+10%2E1007%2FBF01088832%5D+%E2%80%94+%5Bdoi%3A10%2E1007%2Fbf01088832%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2Fbf0108)
104. Turon A. Understanding and expressing scalable concurrency [Ph.D. Thesis]. Boston: Northeastern University, 2013. [find](https://scholar.google.com/scholar?q=Turon+A%2E+Understanding+and+expressing+scalable+concurrency+%5BPh%2ED%2E+Thesis%5D%2E+Boston%3A+Northeastern+University%2C+2013%2E)
105. Michael MM, Scott ML. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proc. of the 15th Annual ACM Symp. on Principles of Distributed Computing. Philadelphia: ACM, 1996. 267–275. [doi: 10.1145/248052.248106] — [doi:10.1145/248052.248106](https://doi.org/10.1145/248052.248106) [find](https://scholar.google.com/scholar?q=Michael+MM%2C+Scott+ML%2E+Simple%2C+fast%2C+and+practical+non%2Dblocking+and+blocking+concurrent+queue+algorithms%2E+In%3A+Proc%2E+of+the+15th+Annual+ACM+Symp%2E+on+Principles+of+Distributed+Computing%2E+Philadelphia%3A+AC)
106. Folly: Facebook open-source library. 2020. [https://github.com/facebook/folly](https://github.com/facebook/folly) [↗](https://github.com/facebook/folly)
107. Treiber RK. Systems programming: Coping with parallelism. New York: Int’l Business Machines Incorporated, Thomas J. Watson Research Center, 1986. [find](https://scholar.google.com/scholar?q=Treiber+RK%2E+Systems+programming%3A+Coping+with+parallelism%2E+New+York%3A+Int%E2%80%99l+Business+Machines+Incorporated%2C+Thomas+J%2E+Watson+Research+Center%2C+1986%2E)
108. Frumin DAN, Krebbers R, Birkedal L. Reloc reloaded: Technical appendix. Technical Report, 2020. [https://cs.ru.nl/~dfrumin/reloc/tech-](https://cs.ru.nl/~dfrumin/reloc/tech-) [↗](https://cs.ru.nl/~dfrumin/reloc/tech-)