| References: [1] Abadi, M. & Lamport, L. (1993) Composing specifications. ACM Transactions on Programming Languages and Systems, 15, 73–132 [DOI: 10.1145/151646.151649].
[2] Aeronautical Radio, Inc. & ARINC (2015). Specification 653: Avionics Application Software Standard Interface, Part 1–Required Services. ARINC Airlines Electronic Engineering Committee.
[3] Ahman, D. & Pretnar, M. (2021) Asynchronous effects. Proceedings of the ACM on Programming Languages. Proceedings of the ACM Program. Lang, 5, 1–28 [DOI: 10.1145/3434305].
[4] Bauer, A. & Pretnar, M. (2015) Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming. Algebraic Methods Program, 84, 108–123 [DOI: 10.1016/j.jlamp.2014.02.001].
[5] Chaochen, Z., Hoare, C.A.R. & Ravn, A.P. (1991) A calculus of durations. Information Processing Letters, 40, 269–276 [DOI: 10.1016/0020-0190(91)90122-X].
[6] Chou, C.-T., Mannava, P.K. & Park, S. (2004) A simple method for parameterized verification of cache coherence protocols. In: Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin, TX, USA, 15–17 November, 2004, Proceedings, pp. 382–398.
[7] Cock, D., Klein, G. & Sewell, T. (2008) Secure microkernels, state monads and scalable refinement. In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, 18–21 August, 2008. Proceedings, pp. 167–182 [DOI: 10.1007/978-3-540-71067-7_16].
[8] Dean, J. & Ghemawat, S. (2008) MapReduce: Simplified data processing on large clusters. Communications of the ACM, 51, 107–113 [DOI: 10.1145/1327452.1327492].
[9] Foster, S. (2019), Proceedings Hybrid relations in isabelle/utp. In: Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Vol. 8. October: Porto, Portugal, pp. 130– 153.
[10] Foster, S., Baxter, J., Cavalcanti, A., Miyazawa, A. & Woodcock, J. (2018) Automating verification of state machines with reactive designs and isabelle/utp. In: Proceedings Formal Aspects of Component Software - 15th International Conference, FACS 2018, Pohang, South Korea, 10–12 October, 2018, pp. 137–155.
[11] Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J. & Zeyda, F. (2020) Unifying semantic foundations for automated verification tools in Isabelle/UTP. Science of Computer Programming, 197, 102510 [DOI: 10.1016/j.scico.2020.102510].
[12] Greenaway, D. (2014). Automated Proof-Producing Abstraction of C Code. URL: handle.unsw.edu.au/1959.4/54260 [PhD Thesis]. University of New South Wales: Sydney. International Journal of Computational Linguistics Research Volume 14 Number 28 1 March 2023
[13] Gu, R., Shao, Z., Chen, H., Wu, Xiongnan (N), Kim, J., Sjöberg, V. & Costanzo, D. (2016) Certikos: An extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, 2–4 November, Vol. 2016. URL: https://www.usenix.org/conference/osdi16/technical-sessions/ presentation/gu, pp. 653–669.
[14] Guo, X., Lesourd, M., Liu, Mengqi, Rieg, L. & Shao, Z. (2019) Integrating formal schedulability analysis into a verified OS kernel. In: Proceedings, Part II Computer Aided Verification - 31st International Conference, CAV 2019, New York City, USA, 15–18 July, 2019, pp. 496–514 [DOI: 10.1007/978-3-030-25543-5_28].
[15] Halpern, J.Y., Manna, Z. & Moszkowski, B.C. (1983) A hardware semantics based on temporal intervals. In: Automata, Languages and Programming, 10th Colloquium, Barcelona, Spain. Proceedings. ITP Foundation 2022, 1983, 278–291 [DOI: 10.1007/BFb0036915].
[16] Maximilian P. L. Haslbeck and Peter Lammich. For a few dollars more - verified fine-grained algorithm analysis down to LLVM. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, pages 292–319, 2021.
[17] C.A.R Hoare and Jifeng He. Unifying Theories of Programming. Prentice-Hall, 1998.
[18] Gerwin Klein. Operating system verification–an overview. Sadhana, 34:27–69, 2009.
[19] Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst., 32(1): 2:1–2:70, 2014. doi:10.1145/2560537.
[20] Jérémie Koenig and Zhong Shao. Refinement-based game semantics for certified abstraction layers. In LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 633–647, 2020. doi:10.1145/3373718.3394799.
[21] Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. From C to interaction trees: specifying, verifying, and testing a networked server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 234–248, 2019. doi:10.1145/3293880.3294106.
[22] Peter Lammich. Refinement to imperative HOL. J. Autom. Reason., 62(4):481–503, 2019.
[23] Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to hopcroft’s algorithm. In Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pages 166– 182, 2012.
[24] Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, and Guillaume Hiet. Modular verification of programs with effects and effects handlers. Formal Aspects Comput., 33(1):127–150, 2021. doi:10.1007/s00165-020-00523-2.
[25] Mengqi Liu, Lionel Rieg, Zhong Shao, Ronghui Gu, David Costanzo, Jung-Eun Kim, and Man-Ki Yoon. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. Proc. ACM Program. Lang., 4(POPL):20:1–20:31, 2020. doi:10.1145/ 3371088.
[26] Nancy A. Lynch and Eugene W. Stark. A proof of the Kahn principle for input/output automata. Inf. Comput., 82(1):81–92, 1989. doi:10.1016/0890-5401(89)90066-7.
[27] Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, Vancouver, British Columbia, Canada, August 10-12, 1987, pages 137–151, 1987. doi:10. 1145/41840.41852.
[28] Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, International Journal of Computational Linguistics Research Volume 14 Number 1 March 2023 29 and Gerwin Klein. sel4: From general purpose to a proof of information flow enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013, pages 415–429, 2013.
[29] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9.
[30] Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, York, UK, March 22-29, 2009. Proceedings, pages 80–94, 2009. doi:10.1007/ 978-3-642-00590-9_7.
[31] John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55–74, 2002. doi:10.1109/ LICS.2002.1029817.
[32] Frédéric Tuong and Burkhart Wolff. Clean - an abstract imperative programming language and its theory. Arch. Formal Proofs, 2019, 2019. URL: https://www.isa-afp.org/entries/ Clean.html. B. Zhan, Y. Lv, S. Wang, G. Zhao, J. Hao, H. Ye, and B. Xia 33:21
[33] Freek Verbeek, Oto Havle, Julien Schmaltz, Sergey Tverdyshev, Holger Blasum, Bruno Langenstein,Werner Stephan, BurkhartWolff, and Yakoub Nemouchi. Formal API specification of the pikeos separation kernel. In NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, pages 375–389, 2015.
[34] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1–51:32, 2020. doi:10.1145/3371119.
[35] Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. A practical verification framework for preemptive OS kernels. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, pages 59–79, 2016. doi:10.1007/978-3-319-41540-6_4.
[36] Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. Verifying an HTTP key-value server with interaction trees and VST. In 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), pages 32:1– 32:19, 2021.
[37] Yongwang Zhao and David Sanán. Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, pages 515–533, 2019. doi:10.1007/978-3-030-25543-5_29.
[38] Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. Reasoning about information flow security of separation kernels with channel-based communication. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 791–810, 2016.
[39] Yongwang Zhao, David Sanán, Fuyuan Zhang, and Yang Liu. A parametric rely-guarantee reasoning framework for concurrent reactive systems. In Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, pages 161–178, 2019. doi:10.1007/978-3-030-30942-8_11.
[40] Yongwang Zhao, Zhibin Yang, and Dianfu Ma. A survey on formal specification and verification of separation kernels. Frontiers Comput. Sci., 11(4):585–607, 2017. doi: 10.1007/s11704-016-4226-2. |
