Proving correctness of JavaCard DL taclets using Bali

Date

2005

Authors

Trentleman, Kerry

Journal Title

Journal ISSN

Volume Title

Publisher

IEEE Computer Society

Abstract

Developed at the University of Karlsruhe, KeY is an augmented commercial CASE tool with specification and deductive verification functionalities. Recently, lightweight, stand-alone tactics or taclets have been introduced in order to implement the JavaCard

Description

Keywords

Keywords: Deductive verification; Dynamic logic; Isabelle; Sequent calculus; Taclets; Theorem provers; Biomineralization; Differentiation (calculus); Formal logic; Semantics; Smart cards; Theorem proving; Software engineering

Citation

URI

http://hdl.handle.net/1885/39126

Collections

ANU Research Publications

Source

Third IEEE Conference on Software Engineering and Formal Methods (SEFM 2004) Proceedings

Type

Conference paper

Book Title

Entity type

Access Statement

License Rights

DOI

10.1109/SEFM.2005.37

Restricted until

DSpace software copyright © 2002-2026 LYRASIS