Abstract
In this paper we extend a program logic for verifying JAVA CARD applications by introducing a "throughout" operator that allows us to prove "strong" invariants. Strong invariants can be used to ensure "rip out" properties of JAVA CARD programs (properties that are to be maintained in case of unexpected termination of the program). Along with introducing the "throughout" operator, we show how to handle the JAVA CARD transaction mechanism (and, thus, conditional assignments) in our logic. We present sequent calculus rules for the extended logic. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Beckert, B., & Mostowski, W. (2003). A program logic for handling JAVA CARD’s transaction mechanism. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2621, 246–260. https://doi.org/10.1007/3-540-36578-8_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
