Certification Using the Mobius Base Logic

DOI10.1007/978-3-540-92188-2_2MaRDI QIDQ3602993zbMATH OpenOpenAlexFDO

Authors Lennart Beringer, Martin Hofmann, Mariela Pavlova

Publication date 12 February 2009

Published in Formal Methods for Components and Objects (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-92188-2_2

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• Justification logic as a foundation for certifying mobile computation
• Abstract interpretation-based mobile code certification
• A Certified Distributed Security Logic for Authorizing Code
• Certificate Translation in Abstract Interpretation

Cites work

• A Bytecode Logic for JML and Types
• A program logic for handling Java Card's transaction mechanism
• A program logic for resource verification
• FM 2005: Formal Methods
• Hoare logics for recursive procedures and unbounded nondeterminism
• scientific article; zbMATH DE number 2163030 (Why is no real title available?)
• Integration of a Security Type System into a Program Logic
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic for Programming, Artificial Intelligence, and Reasoning
• Precise interprocedural analysis through linear algebra
• Proof-carrying code from certified abstract interpretation and fixpoint compression
• Simplify: a theorem prover for program checking
• Sometime = always + recursion always. On the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs
• Verification, Model Checking, and Abstract Interpretation

Cited in

(7)

• Verifying pointer and string analyses with region type systems
• Certificates and Separation Logic
• The Logic of Proofs as a Foundation for Certifying Mobile Computation
• A Certified Distributed Security Logic for Authorizing Code
• Justification logic as a foundation for certifying mobile computation
• Secure Prolog-based mobile code
• Relational bytecode correlations

Describes a project that uses

Uses Software

• SIMPLIFY

This page was built for publication: Certification Using the Mobius Base Logic

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