An overview of the K semantic framework

By Grigore Roşu, Traian-Florin Serbanuta. J. Log. Algebraic Methods Program., 2010

472 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Blockchain-Enabled Smart Contracts: Architecture, Applications, and Future Trends (2019, methodology): “[56] presented KEVM, an executable formal specification of the EVM bytecode stack-based language built with the K Framework [57], which designed to serve as a solid foundation for further formal analyses.”
Smart Contract Development: Challenges and Opportunities (2021, methodology): “also developed KEVM, a formal semantics of the EVM in the K framework [121], [25]; and further evaluated its effectiveness in verifying EVM smart contracts [59], [114].”
KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine (2018, methodology): “We now provide some required background for our work, including a high-level overview of smart contracts, the EVM smart contract language, and the K Framework.”
A Survey on Ethereum Systems Security (2019, methodology): “[143] (25) present a complete semantics of the EVM, referred to as KEVM, using the K framework [144] to achieve language-independent program verification.”
Learning to Fuzz from Symbolic Execution with Application to Smart Contracts (2019, methodology): “KEVM [28] is an executable formal specification of EVM bytecode in the K Framework [50].”