Local temporal reasoning
Local temporal reasoning
复制标题
DOI：
10.1145/2603088.2603138
复制
发表时间：
2014-07
期刊：
影响因子：
--
通讯作者：
Eric Koskinen;Tachio Terauchi
中科院分区：
文献类型：
--
作者：
Eric Koskinen;Tachio Terauchi
我们提出了第一种推理高阶、无限数据程序的时序逻辑属性的方法。通过区分规范中的有限跟踪和无限跟踪，我们获得了一些规则，这些规则允许我们通过类型和效果系统来推理程序部分的时间行为，然后该系统能够将这些事实组合在一起以证明程序的整体目标属性。仅类型系统就足够强大，可以使用细化类型和时间效应导出许多时间安全属性。我们还展示了如何使用现有技术作为预言机来提供有关程序部分的活跃信息（例如终止），并且类型和效果系统可以将此信息与时间安全信息结合起来以导出重要的时间属性。我们的工作应用于高阶软件的验证以及程序程序的模块化策略。
We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs.