基于跟踪的演绎验证（技术报告）
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
