A proof system for abstract non-interference

DOI10.1093/LOGCOM/EXP053MaRDI QIDQ3553917zbMATH OpenOpenAlexWikidataFDO

Authors Roberto Giacobazzi, Isabella Mastroeni

Publication date 21 April 2010

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/a5aff6308b6e3c3aaf50e5c52b5d30896df4435c

zbMATH Keywords

abstract domainsabstract interpretationclosure operatorslogic of programsnon-interferencesemanticsstatic program analysisverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Computer Science Logic
• Abstract non-interference
• Typed Lambda Calculi and Applications
• Proving concurrent noninterference
• Decidability and proof systems for language-based noninterference relations

Cited in

(13)

• Redundant proofs of non-interference in Levin-Gries CSP program proofs
• An implementation-theoretic approach to non-cooperative foundations
• Abstract Certification of Global Non-interference in Rewriting Logic
• scientific article; zbMATH DE number 3890097 (Why is no real title available?)
• Abstract non-interference
• Non-interference Properties for Data-Type Reduction of Communicating Systems
• Proving concurrent noninterference
• Abstract interpretation-based approaches to security -- a survey on abstract non-interference and its challenging applications
• Computer Science Logic
• Decidability and proof systems for language-based noninterference relations
• Programming Languages and Systems
• Typed Lambda Calculi and Applications
• Improving dynamic code analysis by code abstraction

This page was built for publication: A proof system for abstract non-interference

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