一句话：提出 SPECTRA，融合符号执行、抽象解释与 SMT 验证，为 Solidity 合约自动推断函数级行为规约并检测漏洞。
智能合约安全分析常缺乏显式行为规约，导致漏洞检测与理解困难。SPECTRA 是一个面向 Solidity 合约的静态分析框架，集成符号执行、七域抽象解释、语义漏洞检测、规约合成、SMT 验证与 CEGAR 精化，以自动推断函数级行为规约并发现漏洞。作者在 220 个合约上评估：成功分析 216 个（98.18%），推断出 1,381 条函数级规约（每个成功合约平均 6.39 条），在 192 个合约（88.89%）中报告 673 个漏洞发现，中位运行时间为 0.70 秒。结果表明，面向规约的分析在基准规模上具有实际可行性。
SPECTRA is a static-analysis framework for Solidity contracts that integrates symbolic execution, seven-domain abstract interpretation, semantic vulnerability detection, specification synthesis, SMT validation, and CEGAR refinement. Across 220 contracts, SPECTRA analyzes 216 (98.18%), infers 1,381 function-level specifications (6.39 per successful contract), and reports 673 vulnerability findings in 192 contracts (88.89%), with 0.70 s median runtime. These results indicate that specification-oriented analysis remains practical at benchmark scale.
@inproceedings{ZhangLRHT26a,
title = {SPECTRA: Specification-Oriented Static Analysis for Smart Contract Security and Behavioral Contract Inference},
author = {Haoyi Zhang and Tianfeng Liang and Huaijin Ran and Md Maruf Hasan and Xunzhu Tang},
booktitle = {FSE},
year = {2026},
doi = {10.1145/3803437.3807384}
}