B\"uchi Types for Infinite Traces and Liveness
Logic in Computer Science
2014-01-22 v1 Programming Languages
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.
Keywords
Cite
@article{arxiv.1401.5107,
title = {B\"uchi Types for Infinite Traces and Liveness},
author = {Martin Hofmann and Wei Chen},
journal= {arXiv preprint arXiv:1401.5107},
year = {2014}
}