Büchi Types for Infinite Traces and Liveness

Martin Hofmann, Wei Chen

Research output: Working paper


We develop a new type and effect system based on B\"uchi automata to capture finite and infinite traces produced by programs in a small language which allows non-deterministic choices and infinite recursions. There are two key technical contributions: (a) an abstraction based on equivalence relations defined by the policy B\"uchi automaton, the B\"uchi abstraction; (b) a novel type and effect system to correctly capture infinite traces. We show how the B\"uchi abstraction fits into the abstract interpretation framework and show soundness and completeness.
Original languageEnglish
Number of pages24
Publication statusPublished - Oct 2013

Cite this