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.
Securify: Practical security analysis of smart contracts
5 Pith papers cite this work. Polarity classification is still indexing.
5
Pith papers citing it
citation-role summary
background 3
citation-polarity summary
verdicts
UNVERDICTED 5roles
background 3representative citing papers
Chaintrix achieves 71.7% recall on 120 high-severity vulnerabilities in the EVMbench benchmark and outperforms the strongest frontier-model baseline by 26 percentage points through LLM pipelines grounded in a Cross-Contract Interaction Model and filtered by structural checks.
The paper examines denial-of-service risks to multi-round transaction simulation arising from inter-transaction dependencies in smart-contract state.
OpDiffer applies LLMs and static analysis to opcode-level differential testing of EVMs, reporting 26 previously unknown bugs across nine implementations along with coverage gains and an estimate that 7.21% of real contracts could trigger the bugs.
A formal coordination model with dynamic roles and data-driven transitions enables a toolchain for validating models, generating Solidity smart contracts, and synthesizing tests.
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.
-
CHAINTRIX: A multi-pipeline LLM-augmented framework for automated smart-contract security auditing
Chaintrix achieves 71.7% recall on 120 high-severity vulnerabilities in the EVMbench benchmark and outperforms the strongest frontier-model baseline by 26 percentage points through LLM pipelines grounded in a Cross-Contract Interaction Model and filtered by structural checks.
-
Position Paper: Denial-of-Service against Multi-Round Transaction Simulation
The paper examines denial-of-service risks to multi-round transaction simulation arising from inter-transaction dependencies in smart-contract state.
-
OpDiffer: LLM-Assisted Opcode-Level Differential Testing of Ethereum Virtual Machine
OpDiffer applies LLMs and static analysis to opcode-level differential testing of EVMs, reporting 26 previously unknown bugs across nine implementations along with coverage gains and an estimate that 7.21% of real contracts could trigger the bugs.
-
Automatic Code and Test Generation of Smart Contracts from Coordination Models
A formal coordination model with dynamic roles and data-driven transitions enables a toolchain for validating models, generating Solidity smart contracts, and synthesizing tests.