Automatic inference of access permissions

DOI10.1007/978-3-642-27940-9_14MaRDI QIDQ2891412zbMATH OpenOpenAlexFDO

Authors Pietro Ferrara, Peter Müller

Publication date 15 June 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-27940-9_14

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Permission inference for array programs
• Viper: a verification infrastructure for permission-based reasoning
• Permission accounting in separation logic
• A concurrent constraint programming interpretation of access permissions
• Syntactic control of interference for separation logic

Cites work

• A Basis for Verifying Multi-threaded Programs
• Compositional shape analysis by means of bi-abduction
• Grammar Analysis and Parsing by Abstract Interpretation
• scientific article; zbMATH DE number 1617328 (Why is no real title available?)
• scientific article; zbMATH DE number 1693447 (Why is no real title available?)
• scientific article; zbMATH DE number 1953020 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• Permission accounting in separation logic
• Polymorphic Fractional Capabilities
• Programming Languages and Systems
• Programming Languages and Systems
• Separation logic and abstraction
• Static contract checking with abstract interpretation
• Systematic design of program transformation frameworks by abstract interpretation
• The Daikon system for dynamic detection of likely invariants
• Verifying properties of parallel programs

Cited in

(4)

• Viper: a verification infrastructure for permission-based reasoning
• A type system for borrowing permissions
• A concurrent constraint programming interpretation of access permissions
• Permission inference for array programs

Describes a project that uses

Uses Software

• Houdini
• Chalice
• VeriFast
• Daikon
• VeriCool
• TVLA

This page was built for publication: Automatic inference of access permissions

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