论文标题
迈向基于痕量的演绎验证（技术报告）
Towards Trace-based Deductive Verification (Tech Report)
论文作者
论文摘要
根据前和后条件指定程序行为的合同对于可扩展的软件验证至关重要，但不能对执行过程中发生的事件表示任何约束。这需要用中间断言注释代码，从而防止全文抽象。 我们对能够以模块化方式指定递归过程的符号痕迹提出了逻辑，该过程仅指定的程序在事件方面。我们还提供了基于符号执行和归纳的扣除系统，与痕量语义相比，我们被证明是合理的。 我们的工作将基于合同的基于痕量的演绎验证推广。
Contracts specifying a procedure's behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification.
