Dependent Temporal Effects and Fixpoint Logic for Verification

Authors: Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio Terauchi

Paper Information

Title:Dependent Temporal Effects and Fixpoint Logic for Verification
Authors:Yoji Nanjo, Hiroshi Unno, Eric Koskinen and Tachio Terauchi
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:higher-order programs, temporal verification, fixpoint logic, dependent temporal effects, dependent refinement types

ABSTRACT. Existing approaches to temporal verification of higher-order functional programs have either sacrificed compositionality in favor of achieving automation or vice-versa. In this paper we present a dependent-refinement type \& effect system to ensure that well-typed programs satisfy given temporal properties, and also give an algorithmic approach---based on deductive reasoning over a fixpoint logic---to typing in this system. The first contribution is a novel type-and-effect system capable of expressing \emph{dependent temporal} effects, which are fixpoint logic predicates on event sequences and program values, extending beyond the (non-dependent) temporal effects used in recent proposals. Temporal effects facilitate compositional reasoning whereby the temporal behavior of program parts are summarized as effects and combined to form those of the larger parts. As a second contribution, we show that type checking and typability for the type system can be reduced to solving first-order fixpoint logic constraints. Finally, we present a novel deductive system for solving such constraints. The deductive system consists of rules for reasoning via invariants and well-founded relations, and is able to reduce formulas containing both least and greatest fixpoints to predicate-based reasoning.

Talk:Jul 11 11:40 (Session 64E)