Automated Temporal Verification of Integrated Dependent Effects.

Existing approaches to temporal verification have either sacrificed compositionality in favor of achieving automation or vice-versa. To exploit the best of both worlds, we present a new solution to ensure temporal properties via a Hoare-style verifier and a term rewriting system (T.r.s) on Integrated Dependent Effects. The first contribution is a novel effects logic capable of integrating value-dependent finite and infinite traces into a single disjunctive form, resulting in more concise and expressive specifications. As a second contribution, by avoiding the complex translation into automata, our purely algebraic T.r.s efficiently checks the language inclusion, relying on both inductive and coinductive definitions. We demonstrate the feasibility of our method using a prototype system and a number of case studies. Our experimental results show that our implementation outperforms the automata-based model checker PAT by 31.7% of the average computation time.