分离逻辑

1. ITP

   Mechanised Separation Algebra Klein, Gerwin, Kolanski, Rafal, and Boyton, Andrew In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings 2012
2. ITP

   Proof Tactics for Assertions in Separation Logic Hou, Zhe, Sanán, David, Tiu, Alwen, and Liu, Yang In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brası́lia, Brazil, September 26-29, 2017, Proceedings 2017
3. ICFP

   Separation logic for sequential programs (functional pearl) Charguéraud, Arthur Proc. ACM Program. Lang. 2020
4. APLAS

   Bringing Order to the Separation Logic Jungle Cao, Qinxiang, Cuellar, Santiago, and Appel, Andrew W. In Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings 2017
5. JAR

   VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs Cao, Qinxiang, Beringer, Lennart, Gruetter, Samuel, Dodds, Josiah, and Appel, Andrew W. J. Autom. Reason. 2018

并发程序逻辑

1. FASE

   Owicki/Gries in Isabelle/HOL Nipkow, Tobias, and Nieto, Leonor Prensa In Fundamental Approaches to Software Engineering, Second Internationsl Conference, FASE’99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings 1999
2. ESOP

   The Rely-Guarantee Method in Isabelle/HOL Nieto, Leonor Prensa In Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings 2003
3. CPP

   Complx: a verification framework for concurrent imperative programs Amani, Sidney, Andronick, June, Bortin, Maksym, Lewis, Corey, Rizkallah, Christine, and Tuong, Joseph In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017 2017
4. TACAS

   CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs Sanán, David, Zhao, Yongwang, Hou, Zhe, Zhang, Fuyuan, Tiu, Alwen, and Liu, Yang In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I 2017
5. FM

   A Parametric Rely-Guarantee Reasoning Framework for Concurrent Reactive Systems Zhao, Yongwang, Sanán, David, Zhang, Fuyuan, and Liu, Yang In Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings 2019