2014/01/20 by Martin Hofmann, Wei Chen, Hofmann, Martin +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.LO #cs.PL #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1401.5107
arxiv created 2014/01/20 · openalex publication_date 2014/01/20 · arxiv updated 2014/01/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We develop a new type and effect system based on Büchi 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üchi automaton, the Büchi abstraction; (b) a novel type and effect system to correctly capture infinite traces. We show how the Büchi abstraction fits into the abstract interpretation framework and show soundness and completeness.