[1] N. Satoshi, “Bitcoin: A Peer-to-Peer Electronic Cash System,” 2008 [2] C. Cadar, D. Dunbar,D. Engler, “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,” inProceedings of 8th USENIX Symposium on Operating Systems Design and Implementation Conference, 2008 [3] The Coq Development Team, The Coq Proof Assistant, (http://coq.inria.fr, accessed 1999 - 2018 [4] M. Norrish, “C Formalised in HOL,” PhD Thesis, Computer Laboratory, University of Cambridge, 1998 [5] S. S.Ishtiaq and P. W. O'Hearn, “BI as an Assertion Language for Mutable Data Structures,” in Proceedings of the 28th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 2001), Vol. 36, pp. 14-26, ACM, 2001 [6] H. Tuch, G. Klein,M. Norrish, “Types, Bytes, and Separation Logic,” inM. Hofmann and M. Felleisen, Editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), pp. 97-108, ACM, January 2007 [7] A. W.Appel and S. Blazy, “Separation Logic for Small-Step Cminor,” in K. Schneider and J. Brandt, Editors, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2007), Vol. 4732, pp. 5-21, Springer, September 2007 [8] J. Manson, W. Pugh,S. V. Adve, “The Java Memory Model,”POPL, 2004 [9] L. Xavier, “The CompCert Verified Compiler,” Documentation and User's Manual, INRIA Paris-Rocquencourt, 2012 [10] A. W. Appel, “Verified Software Toolchain,”ESOP, Vol. 11, 2011 [11] R. H. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. N. Wu,S. C. Weng, “Deep Specifications and Certified Abstraction Layers,” ACM SIGPLAN Notices, Vol. 50. No. 1. ACM, 2015 [12] L. D.Moura and N. Bjørner, “Z3: An Efficient SMT Solver,”Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, 2008 [13] B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds, et al., “SMTCoq: A Plug-in for Integrating SMT Solvers into Coq,” in Proceedings of International Conference on Computer Aided Verification, Springer, Cham, 2017 [14] X. Leroy, “The CompCert Verified Compiler,” Documentation and User's Manual, INRIA Paris-Rocquencourt, 2012 [15] R. O'Connor, “Simplicity: A New Language for Blockchains,”CoRR abs/1711.03028, 2017 [16] P. Wadler, “Comprehending Monads,” LISP and Functional Programming, 1990 [17] Z. Yang and H. Lei, “A General Formal Memory Framework in Coq for Verifying the Properties of Programs based on Higher-Order Logic Theorem Proving with Increased Automation, Consistency, and Reusability,” (https://arxiv.org/abs/1803.00403, accessed 23 April 2018) [18] Z. Yang and H. Lei, “A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts,” (https://arxiv.org/abs/1902.08726, accessed February 2019) [19] Z. Yang and H. Lei, “Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language,” (https://arxiv.org/abs/1803.09885, accessed February 2019) [20] Ethereum, “Ethereum Solidity Documentation,” (https://solidity.readthedocs.io/en/develop/, accessed 2 December 2017) [21] Z. Yang and H. Lei, “FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq,” (https://arxiv.org/abs/1810.04828, accessed Feb. 2019) [22] EOS Blockchain Platform, (https://eos.io/, accessed Apr. 23 2018) |