An abstract interpretation-based model for safety semantics

References

• Abramsky , S. and Jung , A. 1994 . “ Domain theory ” . In Handbook of Logic in Computer Science , Edited by: Abramsky , S. , Gabbay , D. M. and Maibaum , T. S.E. Vol. 3 , 1 – 168 . New York, NY : Oxford University Press, Inc .
   Google Scholar
• Alpern , B. and Schneider , F. B. 1985 . Defining liveness . Inform. Process. Lett. , 21 : 181 – 185 .
   Web of Science ®Google Scholar
• Alpern , B. and Schneider , F. B. 1987 . Recognizing safety and liveness . Distrib. Comp. , 2 : 117 – 126 .
   Google Scholar
• Alpern , B. , Demers , A. J. and Schneider , F. B. 1986 . Safety without stuttering . Inform. Process. Lett. , 23 : 177 – 180 .
   Google Scholar
• Apt , K. R. and Plotkin , G. D. 1986 . Countable nondeterminism and random assignment . J. ACM , 33 : 724 – 767 .
   Google Scholar
• Baier , C. and Kwiatkowska , M. 2000 . On topological hierarchies of temporal properties . Fund. Inform. , 41 : 259 – 294 .
   Google Scholar
• Birkhoff , G. 1967 . Lattice Theory , 3 Providence, , USA AMS Colloquium Publication, AMS
   Google Scholar
• Chang , E. , Manna , Z. and Pnueli , A. Characterization of temporal property classes . Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP ’92) . Edited by: Kuich , W. Vol. 623 , pp. 474 – 486 . Berlin : Springer-Verlag . Lecture Notes in Computer Science
   Google Scholar
• Cortesi , A. , Filé , G. , Giacobazzi , R. , Palamidessi , C. and Ranzato , F. 1997 . Complementation in abstract interpretation . ACM Trans. Program. Lang. Syst. , 19 : 7 – 47 .
   Google Scholar
• Cousot , P. 2002 . Constructive design of a hierarchy of semantics of a transition system by abstract interpretation . Theor. Comput. Sci. , 277 : 47 – 103 .
   Google Scholar
• Cousot , P. and Cousot , R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints . Proceedings of Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL ’77) . pp. 238 – 252 . New York : ACM Press .
   Google Scholar
• Cousot , P. and Cousot , R. 1979 . Constructive versions of Tarski's fixed point theorems . Pacific J. Math. , 82 : 43 – 57 .
   Google Scholar
• Cousot , P. and Cousot , R. Systematic design of program analysis frameworks . Proceedings of Conference Record of the 6th ACM Symposium on Principles of Programming Languages (POPL ’79) . pp. 269 – 282 . New York : ACM Press .
   Google Scholar
• Cousot , P. and Cousot , R. Inductive definitions, semantics and abstract interpretation . Proceedings of Conference Record of the 19th ACM Symposium on Principles of Programming Languages (POPL ’92) . pp. 83 – 94 . New York : ACM Press .
   Google Scholar
• de Bakker , J. 1980 . Mathematical Theory of Program Correctness , Upper Saddle River, NJ : Prentice-Hall International .
   Google Scholar
• Dijkstra , E. 1975 . Guarded commands, nondeterminism and formal derivation of programs . Commun. ACM , 18 : 453 – 457 .
   Web of Science ®Google Scholar
• Dijkstra , E. W. 1976 . A Discipline of Programming , Upper Saddle River, NJ : Prentice-Hall . Series in Automatic Computation
   Google Scholar
• Dwinger , P. 1954 . On the closure operators of a complete lattice . Indag. Math. , 16 : 560 – 563 .
   Google Scholar
• Filé , G. and Ranzato , F. Complementation of abstract domains made easy . Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming (JICSLP ’96) . Edited by: Maher , M. J. pp. 348 – 362 . Cambridge, MA : The MIT Press .
   Google Scholar
• Fong , P. W. Access control by tracking shallow execution history . Proceedings of the 2004 IEEE Symposium on Security and Privacy . pp. 43 – 55 . Washington, DC : IEEE Computer Society .
   Google Scholar
• Giacobazzi , R. and Ranzato , F. Refining and compressing abstract domains . Proceedings of the 24th International Colloquium on Automata, Languages and Programming (ICALP ’97) . Edited by: Goos , G. , Hartmanis , J. and van Leeuwen , J. Vol. 1256 , pp. 771 – 781 . Berlin : Springer-Verlag . Lecture Notes in Computer Science
   Google Scholar
• Giacobazzi , R. , Palamidessi , C. and Ranzato , F. 1996 . Weak relative pseudo-complements of closure operators . Algebra Universalis , 36 : 405 – 412 .
   Web of Science ®Google Scholar
• Giacobazzi , R. , Ranzato , F. and Scozzari , F. 2000 . Making abstract interpretations complete . J. ACM. , 47 : 361 – 416 .
   Google Scholar
• Gierz , G. , Hofmann , K. H. , Keimel , K. , Lawson , J. D. , Mislove , M. and Scott , D. S. 1980 . A Compendium of Continuous Lattices , Berlin : Springer-Verlag .
   Google Scholar
• Gumm , H. P. 1993 . Another glance at the Alpern–Schneider theorem . Inform. Process. Lett. , 47 : 291 – 294 .
   Google Scholar
• Hamlen , K. W. , Morrisett , G. and Schneider , F. B. 2006 . Computability classes for enforcement mechanisms . ACM Trans. Program. Lang. Syst. , 28 : 175 – 205 .
   Google Scholar
• Hoare , C. 1969 . An axiomatic basis for computer programming . Commun. ACM , 12 : 576 – 580 .
   Web of Science ®Google Scholar
• Lamport , L. 1977 . Proving correctness of multiprocess programs . IEEE Trans. Softw. Eng. , 3 : 125 – 143 .
   Web of Science ®Google Scholar
• Lamport , L. 1994 . The temporal logic of actions . ACM Trans. Program. Lang. Syst. , 16 : 872 – 923 .
   Google Scholar
• Ligatti , J. , Bauer , L. and Walker , D. Enforcing non-safety security policies with program monitors . 10th European Symposium on Research in Computer Security (ESORICS) . Edited by: di Vimercati , S. D.C. , Syverson , P. F. and Gollmann , D. Vol. 3679 , pp. 355 – 373 . Berlin : Springer-Verlag . Lecture Notes in Computer Science
   Google Scholar
• Morgado , J. 1962 . Note on complemented closure operators of complete lattices . Port. Math. , 21 : 135 – 142 .
   Google Scholar
• Owiki , S. and Lamport , L. 1982 . Proving liveness properties of concurrent programs . ACM Trans. Program. Lang. Syst. , 4 : 455 – 495 .
   Google Scholar
• Paun , D. O. April 1999 . “ Closure under stuttering in temporal formulas ” . April , Toronto, Ontario : Dept. of Computer Science, University of Toronto . Master's thesis
   Google Scholar
• Plotkin , G. 1981 . A Structural Approach to Operational Semantics , Denmark : DAIMI-19, Aarhus University .
   Google Scholar
• Schneider , F. B. 2000 . Enforceable security policies . Inform. Syst. Secur. , 3 : 30 – 50 .
   Google Scholar
• Shmuely , Z. 1974 . The structure of Galois connections . Pacific J. Math. , 54 : 209 – 225 .
   Web of Science ®Google Scholar
• Sistla , A. P. 1994 . Safety, liveness and fairness in temporal logic, . Form. Aspects Comput. , 6 ( 5 ) : 495 – 511 .
   Google Scholar
• Sistla , A. P. On characterization of safety and liveness properties in temporal logic . Proceedings of the 4th ACM Symposium on Principles of Distributed Computing . Edited by: Malcolm , M. and Strong , R. New York : ACM Press .
   Google Scholar
• Smyth , M. B. 1992 . “ Topology ” . In Handbook of Logic in Computer Science (Vol. 1): Background: Mathematical Structures , Edited by: Abramsky , S. , Gabbay , Dov M. and Maibaum , T. S.E. Vol. 1 , 641 – 761 . New York, NY : Oxford University Press, Inc .
   Google Scholar
• Thomas , W. 1986 . Safety and liveness properties in propositional temporal logic: Characterization and decidability . Schriften Zur Informatik, Bericht , 116
   Google Scholar