An encoding of Solidity contracts and first-order Hennessy-Milner logic into Lustre enables Kind 2 model checking of complex temporal properties in smart contracts.
In: Proceedings of the 34th Annual Computer Security Applications Conference
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
Annotary is a concolic execution system for smart contract vulnerability detection that uses source-code annotations, symbolic EVM execution, and blockchain data resolution to handle inter-contract and inter-transaction flows.
A controlled comparison of 12 smart contract pairs shows Move reduces security check density by 60% versus Solidity but increases code size by 47%, with developers reporting higher safety confidence in Move despite moderate learning difficulty.
citing papers explorer
-
KindHML: formal verification of smart contracts based on Hennessy-Milner logic
An encoding of Solidity contracts and first-order Hennessy-Milner logic into Lustre enables Kind 2 model checking of complex temporal properties in smart contracts.
-
Annotary: A Concolic Execution System for Developing Secure Smart Contracts
Annotary is a concolic execution system for smart contract vulnerability detection that uses source-code annotations, symbolic EVM execution, and blockchain data resolution to handle inter-contract and inter-transaction flows.
-
Comparing Smart Contract Paradigms: A Preliminary Study of Security and Developer Experience
A controlled comparison of 12 smart contract pairs shows Move reduces security check density by 60% versus Solidity but increases code size by 47%, with developers reporting higher safety confidence in Move despite moderate learning difficulty.