.png){kind=icon}
返回
Operational Semantics for Crystality: A Smart Contract Language for Parallel EVMs
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-031-98208-8_18.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
对可扩展区块链的日益增长的需求推动了智能合约并行执行模型的研究。Crystality是一种为并行以太坊虚拟机（EVMs）设计的创新型智能合约编程语言，通过可编程合约作用域和异步函数转发实现细粒度并发。本文为Crystality提供了第一种形式化的结构化操作语义，为分析其执行提供了严谨的框架。我们在定理证明辅助工具Coq中形式化验证了Crystality的语法和语义，实现了正确性属性的正式验证。作为一个案例研究，我们验证了一个简化的代币转移函数，展示了我们的语义在确保智能合约正确性方面的适用性。我们的工作为形式化验证的并行智能合约奠定了基础，为区块链系统的安全性和可扩展性做出了贡献。
Keyword:
Operational Semantics
Blockchain
Smart Contract
Parallel Execution
Parallel EVMs
Coq
Formal Verification
期刊
T
IF:
0
论文数:
17
被引数:
0
机构
引用论文
X. Qi, J. Jiao, Y. Li, Smart contract parallel execution with fine-grained State accesses, 2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS), 2023: pp. 841–852. https://doi.org/10.1109/ICDCS57875.2023.00068.X. Qi, J. Jiao, Y. Li, 细粒度状态访问的智能合约并行执行, 2023年IEEE第43届国际分布式计算系统会议(ICDCS), 2023: 第841–852页. https://doi.org/10.1109/ICDCS57875.2023.00068..png)
IF0
PREAI
分享收藏
查看更多内容