A unified proof technique for verifying program correctness with big-step semantics
- 1 March 2023
- journal article
- research article
- Published by Elsevier BV in Journal of Systems Architecture
Abstract
No abstract availableKeywords
Funding Information
- Capital Normal University
- National Natural Science Foundation of China
- Ministry of Science and Technology of the People's Republic of China
- Beijing Municipal Education Commission
This publication has 15 references indexed in Scilit:
- eThor: Practical and Provably Sound Static Analysis of Ethereum Smart ContractsPublished by Association for Computing Machinery (ACM) ,2020
- End-to-End Formal Verification of Ethereum 2.0 Deposit Smart ContractPublished by Springer Science and Business Media LLC ,2020
- Theoretical and Practical Approaches to the Denotational Semantics for MDESL based on UTPFormal Aspects of Computing, 2020
- VerX: Safety Verification of Smart ContractsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2020
- Blockchain technology overviewPublished by National Institute of Standards and Technology (NIST) ,2018
- ZEUS: Analyzing Safety of Smart ContractsPublished by Internet Society ,2018
- Semantics-based program verifiers for all languagesPublished by Association for Computing Machinery (ACM) ,2016
- A UTP semantics for CircusFormal Aspects of Computing, 2007
- Guarded commands, nondeterminacy and formal derivation of programsCommunications of the ACM, 1975
- An axiomatic basis for computer programmingCommunications of the ACM, 1969