Abstract
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 language | English |
|---|---|
| Publisher | ArXiv |
| Number of pages | 24 |
| Publication status | Published - Oct 2013 |