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
Collections
Source
Third IEEE Conference on Software Engineering and Formal Methods (SEFM 2004) Proceedings
Type
Conference paper