A dynamic logic for the formal verification of Java card programs

DOI10.1007/3-540-45165-X_2MaRDI QIDQ2771739zbMATH OpenFDO

Authors Bernhard Beckert

Publication date 18 February 2002

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2041/20410006

Mathematics Subject Classification ID

Theory of programming languages (68N15) Data encryption (aspects in computer science) (68P25) Computing methodologies and applications (68U99)

Review text

Summay:In this paper, we define a program logic (an instance of Dynamic Logic) for formalising properties of JAVA CARD programs, and we give a sequent calculus for formally verifying such properties. The purpose of this work is to provide a framework for software verification that can be integrated into real-world software development processes. For the entire collection see [Zbl 0968.68557].

Recommendations

• Fundamental Approaches to Software Engineering
• Algebraic Methodology and Software Technology
• Formal specification and verification of JavaCard's application identifier class
• An architecture for interactive program provers
• Formal methods in context: security and Java card

Cited in

(17)

• Formal verification of a programming logic for a distributed programming language
• Correctness of Java card method lookup via logical relations
• An exercise on the generation of many-valued dynamic logics
• A program logic for resources
• Formal methods in context: security and Java card
• Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• scientific article; zbMATH DE number 1956492 (Why is no real title available?)
• Verification conditions for source-level imperative programs
• scientific article; zbMATH DE number 2090143 (Why is no real title available?)
• Fundamental Approaches to Software Engineering
• Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic
• Verification by Parallelization of Parametric Code
• KeY: A Formal Method for Object-Oriented Systems
• FM 2005: Formal Methods
• The rewriting logic semantics project
• Integration of a security type system into a program logic

This page was built for publication: A dynamic logic for the formal verification of Java card programs

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