Elamur Research⌕
☰
home / papers / 2024 / 基于交互式定理证明的并发程序验证工作综述

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

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 · Natural language processing

Cite

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.13328/j.cnki.jos.007138

@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}
}

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
  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
  3. Bernstein PA, Hadzilacos V, Goodman N. Concurrency Control and Recovery in Database Systems. Reading: Addison-Wesley, 1987. find
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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 ↗
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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 ↗
  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
  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
  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
  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 ↗
  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
  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
  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
  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
  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
  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
  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
  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
  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
  67. The OpenMP API specifcation for parallel programming, 2020. 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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  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
  82. Mansky W. Bringing Iris into the verified software toolchain. arXiv: 2207.06574, 2022. — [arXiv:2207.06574](https://arxiv.org/abs/2207.06574) find
  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
  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
  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
  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
  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
  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
  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
  90. Donovan AAA, Kernighan BW. The Go Programming Language. Addison-Wesley Professional, 2015. find
  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
  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
  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
  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 ↗
  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
  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
  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
  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
  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
  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
  101. Labrosse J. MicroC/OS-II: The Real Time Kernel. CRC Press, 2002. find
  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
  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
  104. Turon A. Understanding and expressing scalable concurrency [Ph.D. Thesis]. Boston: Northeastern University, 2013. find
  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
  106. Folly: Facebook open-source library. 2020. 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
  108. Frumin DAN, Krebbers R, Birkedal L. Reloc reloaded: Technical appendix. Technical Report, 2020. https://cs.ru.nl/~dfrumin/reloc/tech- ↗

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/papers/wang-2024-interactive-theorem-proving/