You are presented with multiple paper abstracts, alongside the associated literature review and chapter titles. Given the provided information, you are going to do a literature review. Please generate a coherent literature review that synthesizes the content, draws connections between different works, highlights major findings, and identifies any gaps in the existing research.

Literature Review Title: A Survey on Security Verification of Blockchain Smart Contracts 
Chapter Title:  3) SEMANTIC ANALYSIS 
1. Abstract of Cited Paper (BIB001):  In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts. 
2. Abstract of Cited Paper (BIB002):  Currently, Bitcoin and Ethereum are the two most popular cryptocurrency systems, especially Ethereum. It permits complex financial transactions or rules through scripts, which is called smart contracts. Since Ethereum smart contracts hold millions of dollars, their execution correctness is crucial against attacks which aim at stealing the assets. In this paper, we proposed a security assurance method for smart contract source code to find potential security risks. It contains two main functions, the first is syntax topological analysis of smart contract invocation relationship, to help developers to understand their code structure clearly; the second is logic risk (which may lead to vulnerabilities) detection and location, and label results on topology diagram. For developers' convenience, we have built a static analysis tool called SASC to generate topology diagram of invocation relationship and to find potential logic risks. We have made an evaluation on 2,952 smart contracts, experiment results proved that our method is intuitive and effective. 
3. Abstract of Cited Paper (BIB003):  Smart contracts, as a promising and powerful application on the Ethereum blockchain, have been growing rapidly in the past few years. Since they are highly vulnerable to different forms of attacks, their security becomes a top priority. However, existing security auditing techniques are either limited in finding vulnerabilities (rely on pre-defined bug patterns) or very expensive (rely on program analysis), thus are insufficient for Ethereum. To mitigate these limitations, we proposed a novel semantic-aware security auditing technique called S-GRAM for Ethereum. The key insight is a combination of N-gram language modeling and lightweight static semantic labeling, which can learn statistical regularities of contract tokens and capture high-level semantics as well (e.g., flow sensitivity of a transaction). S-GRAM can be used to predict potential vulnerabilities by identifying irregular token sequences and optimize existing in-depth analyzers (e.g., symbolic execution engines, fuzzers etc.). We have implemented S-GRAM for Solidity smart contracts in Ethereum. The evaluation demonstrated the potential of S-GRAM in identifying possible security issues.

Literature Review:
Semantic analysis is another important way to analyze and write a correct contract. Focused on modifying the EVM environment, Hildenbrandt et al.  presented an executable formal specification of the EVM's Bytecode stack-based language called KEVM. It provided a more security environment for the development of the smart contracts, and made the formal analysis of the smart contracts easier. They used the official Ethereum test suite to verify the correctness and performance of the KEVM, which all achieved better results. Daejun et al. BIB002 also proposed a formal verification tool for the EVM Bytecode, which adopted KEVM. Their verification tool had been used to verify various high-profile smart contracts including the ERC20, Ethereum Casper, and DappHub MakerDAO contracts. Focused on developing smart contracts, Zhou et al. BIB003 designed a SASC static analysis tool to generate a syntax topology map of the invocation relationships in smart contracts and mark the locations where risks and vulnerabilities may occur. Liu et al. BIB004 proposed a novel semantic aware security auditing technique called S-gram for Ethereum. They combined the N-gram language to model the static semantic labeling, and predicted potential vulnerabilities by identifying irregular token sequences. Mavridou and Laszka BIB001 introduced FSolidM, a framework rooted in rigorous semantics for designing contracts as FSM. Also, they provided a tool to design the FSM model and verify the correctness of the contracts conveniently. Focused on the published smart contracts, Suiche  designed a decompiler to analyze the syntax and decompile the EVM binary code, so that the readable solidity code was generated. Through static and dynamic analysis of the decompiled code, vulnerabilities in contracts were discovered.