Büchi Types for Infinite Traces and Liveness

Martin Hofmann, Wei Chen

Research output: Working paper

Abstract / Description of output

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


Dive into the research topics of 'Büchi Types for Infinite Traces and Liveness'. Together they form a unique fingerprint.

Cite this