@inbook {IOPORT.05259548,
    author       = {Cousot, Radhia},
    title        = {Abstract interpretation of non-monotone bi-inductive semantic definitions.},
    year         = {2008},
    booktitle    = {Verification, model checking, and abstract interpretation. 9th international conference, VMCAI 2008, San Francisco, USA, January 7--9, 2008. Proceedings},
    isbn         = {978-3-540-78162-2},
    pages        = {1-3},
    publisher    = {Berlin: Springer},
    doi          = {10.1007/978-3-540-78163-9_1},
    abstract     = {Summary: Divergence/nonterminating behaviors definitely need to be considered in static program analysis [13], in particular for typing [2,11]. Divergence information is part of the classical order-theoretic fixpoint denotational semantics [12] but not explicit in small-step/abstract-machine-based operational semantics [14,15,16] and absent of big-step/natural operational semantics [8]. A standard approach is therefore to generate an execution trace semantics from a (labelled) transition system/small-step operational semantics, using either an order-theoretic [3] or metric [19] fixpoint definition or else a categorical definition as a final coalgebra for a behavior functor (modeling the transition relation) up to a weak bisimulation [7,10,18] or using an equational definition for recursion in an order-enriched category [9].},
    identifier   = {05259548},
}