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

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

Recommendations

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

Cites work

• scientific article; zbMATH DE number 1948157 (Why is no real title available?)
• scientific article; zbMATH DE number 1956492 (Why is no real title available?)
• scientific article; zbMATH DE number 2163030 (Why is no real title available?)
• A Bytecode Logic for JML and Types
• FM 2005: Formal Methods
• 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
• Theorem Proving in Higher Order Logics
• Verification, Model Checking, and Abstract Interpretation

Cited in

(7)

• Justification logic as a foundation for certifying mobile computation
• Secure Prolog-based mobile code
• Relational bytecode correlations
• 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

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)