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.
翻译：规定程序前和先决条件的合同行为对于可扩展的软件核查至关重要,但不能对执行程序期间发生的事件表示任何限制。这需要用中间说法来说明代码,防止完全规格抽象化。我们提出了一个关于象征性痕迹的逻辑,以便用模块化的方式具体说明重复性程序,只指特定程序的事件。我们还提供了一个基于象征性执行和诱导的扣减系统,我们证明它与痕量语义相对是可靠的。我们的工作将基于合同的基于追踪的分解核查法概括为基于追踪的分解核查法。
相关内容
微信扫码咨询专知VIP会员