A logic for information flow analysis with an application to forward slicing of simple imperative programs

DOI10.1016/J.SCICO.2006.03.002MaRDI QIDQ859953zbMATH OpenOpenAlexFDO

Authors Torben Amtoft, Anindya Banerjee

Publication date 22 January 2007

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2006.03.002

zbMATH Keywords

abstract interpretationdenotational semanticsHoare logicprogram slicingstrongest postconditionframe ruleinformation flow analysis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• Static Analysis
• A logic for information flow in object-oriented programs
• Information-flow and data-flow analysis of while-programs
• Compile-time detection of information flow in sequential programs
• Simple relational correctness proofs for static analyses and program transformations

Cited in

(12)

• An Independence Relation for Sets of Secrets
• Information flow for Algol-like languages
• From exponential to polynomial-time security typing via principal types
• Abstract program slicing: an abstract interpretation-based approach to program slicing
• Optimality and condensing of information flow through linear refinement
• An independence relation for sets of secrets
• Simple relational correctness proofs for static analyses and program transformations
• Logic of knowledge and discovery via interacting agents -- decision algorithm for true and satisfiable statements
• Logic of secrets in collaboration networks
• A logic for information flow in object-oriented programs
• Logic-flow analysis of higher-order programs
• Abstract semantic dependency

This page was built for publication: A logic for information flow analysis with an application to forward slicing of simple imperative programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q859953)