@TECHREPORT\{IMM2003-02812,
    author       = "F. Nielson and H. R. Nielson and H. Sun",
    title        = "Observation Predicates in Flow Logic",
    year         = "2003",
    number       = "",
    series       = "IMM-Technical Report-2003-23",
    institution  = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/2812-full.html",
    abstract     = "Motivated by the connection between strong and soft type systems we explore flow analyses with hard constraints on the admissible solutions. We show how to use observation predicates and formula rearrangements to map flow analyses with hard constraints into more traditional flow analyses in such a way that the hard constraints are satisfi ed exactly when the observation predicates report no violations. The development is carried out in a large fragment of a first order logic with negation and also takes care of the transformations necessary in order to adhere to the stratification restrictions inherent in Alternation-free Least Fixed Point Logic and similar formalisms such as Datalog."
}