Integration of a security type system into a program logic

DOI10.1016/j.tcs.2008.04.033zbMath1146.68029OpenAlexW2141756654MaRDI QIDQ935469

Jing Pan, Philipp Rümmer, Reiner Hähnle, Dennis Walter

Publication date: 6 August 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.04.033

zbMATH Keywords

formal verificationdynamic logiclanguage-based securityinformation-flow analysissecurity type system

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Abstract Interpretation of Symbolic Execution with Explicit State Updates

Uses Software

• Jif

Cites Work

• A semantic approach to secure information flow
• Verifying persistent security properties
• An Axiomatic Approach to Information Flow in Programs
• Fundamental Approaches to Software Engineering
• On flow-sensitive security types
• Sequential, Parallel, and Quantified Updates of First-Order Structures
• Static Analysis
• Logic for Programming, Artificial Intelligence, and Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item