论文标题
执行时间计划验证限制紧密
Execution Time Program Verification With Tight Bounds
论文作者
论文摘要
本文提出了一个证明系统，用于推理核心命令式编程语言的执行时间范围。针对三种不同的情况定义了证明系统：使用摊销分析，最差的案例执行时间，确切的时间推理的近似值，确切的时间推理以及更少的悲观执行时间估计。我们为这三种情况定义了Hoare逻辑，并证明了其在带注释的成本感知操作语义方面的合理性。最后，我们定义一个验证条件（VC）生成器，该生成器生成证明程序正确性，成本和终止所需的目标。然后将这些目标发送到EasyCrypt工具集进行验证。通过在OCAML中实现将其应用于示例程序所需的不同模块的实现，证明了证明系统的实用性。我们的案例研究是由实时和加密软件激励的。
This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.
