程序的资源分析与验证

以下摘要由 AI 根据胶片自动生成。

本报告从静态、动态、验证三个维度分析程序资源消耗：静态方向基于势能均摊方法自动推导时间复杂度多项式上界，可用于智能合约 gas 预测和拒绝服务漏洞检测。动态方向通过资源制导的符号执行生成触发最坏情况消耗的具体测试输入。验证方向将经典霍尔逻辑的布尔断言推广为非负势函数（量化霍尔逻辑），与分离逻辑结合处理堆结构，并探索基于 Incorrectness Logic 的资源消耗下近似验证。