量化程序分析与验证

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

量化程序分析与验证（Quantitative Program Analysis and Verification）聚焦资源消耗与概率两类可量化性质。静态方向基于势能均摊方法自动推导时间复杂度多项式上界，应用于智能合约 gas 预测和算法复杂性攻击（DoS）检测，动态方向则通过资源制导符号执行生成最坏情况测试输入。验证方向将霍尔逻辑推广为量化霍尔逻辑，结合中心矩分析与集中不等式，可对概率程序（如加密算法）的侧信道信息泄漏风险给出严格上界，并展望了资源感知系统编程语言的设计。